From 09906b09bdb6fe2929d7f63b42381f423824fcc9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 15 Nov 1999 18:35:23 +0000
Subject: Added some greek letters.  A mess if they occur in words.

---
 coq/x-symbol-coq.el | 38 +++++++++++++++++++++++++++++++++++---
 1 file changed, 35 insertions(+), 3 deletions(-)

diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el
index a8c1bfa2..f36d2070 100644
--- a/coq/x-symbol-coq.el
+++ b/coq/x-symbol-coq.el
@@ -2,9 +2,40 @@
   '((longarrowright () "->"  "\\<longrightarrow>")
     (logicaland     () "/\\" "\\<and>")
     (logicalor      () "\\/" "\\<or>")
-    (notsign	    () "~"   "\\<not>")
     (equivalence    () "<->" "\\<equiv>")
-    (existential1   () "EX"  "\\<exists>")))
+    (existential1   () "EX"  "\\<exists>")
+    ;; some naughty ones, but probably what you'd like
+    ;; (a mess in words like "searching" !!)
+    (Gamma  () "Gamma" "\\<Gamma>")
+    (Delta  () "Delta" "\\<Delta>")
+    (Theta  () "Theta" "\\<Theta>")
+    (Lambda () "Lambda" "\\<Lambda>")
+    (Pi     () "Pi" "\\<Pi>")
+    (Sigma  () "Sigma" "\\<Sigma>")
+    (Phi    () "Phi" "\\<Phi>")
+    (Psi    () "Psi" "\\<Psi>")
+    (Omega  () "Omega" "\\<Omega>")
+    (alpha  () "alpha" "\\<alpha>")
+    (beta   () "beta" "\\<beta>")
+    (gamma  () "gamma" "\\<gamma>")
+    (delta  () "delta" "\\<delta>")
+    (epsilon1 () "epsilon" "\\<epsilon>")
+    (zeta   () "zeta" "\\<zeta>")
+    (eta    () "eta" "\\<eta>")
+    (theta1 () "theta" "\\<theta>")
+    (kappa1 () "kappa" "\\<kappa>")
+    (lambda () "lambda" "\\<lambda>")
+;    (mu     () "mu" "\\<mu>")
+;    (nu     () "nu" "\\<nu>")
+    (xi     () "xi" "\\<xi>")
+;    (pi     () "pi" "\\<pi>")
+    (rho    () "rho" "\\<rho>")
+    (sigma  () "sigma" "\\<sigma>")
+    (tau    () "tau" "\\<tau>")
+    (phi1   () "phi" "\\<phi>")
+;    (chi    () "chi" "\\<chi>")
+    (psi    () "psi" "\\<psi>")
+    (omega  () "omega" "\\<omega>")))
 
 ;; All the stuff X-Symbol complains about
 (defvar x-symbol-coq-master-directory 'ignore)
@@ -36,7 +67,8 @@
 (defvar x-symbol-coq-nomule-decode-exec nil)
 (defvar x-symbol-coq-nomule-encode-exec nil)
 
-(message "Coq support for X-Symbol is highly incomplete!  Please help improve it!")
+(warn "Coq support for X-Symbol is highly incomplete!  Please help improve it!
+Send improvements to x-symbol-coq.el to proofgen@dcs.ed.ac.uk")
 
 
 (provide 'x-symbol-coq)
-- 
cgit v1.2.3