# HG changeset patch
# User paulson
# Date 974204808 -3600
# Node ID e6e7205e9e91ac4b2e51782737f3d1e03f2ddc51
# Parent  78168ca704690a0b813295535177f1a2a6f2f539
x-symbol support for Pi, Sigma, -->, : (membership)
  note that "lam" is displayed as TWO lambda-symbols

diff -r 78168ca70469 -r e6e7205e9e91 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Tue Nov 14 13:25:59 2000 +0100
+++ b/src/CTT/Arith.thy	Tue Nov 14 13:26:48 2000 +0100
@@ -14,6 +14,12 @@
 consts "#+","-","|-|"   :: "[i,i]=>i"   (infixr 65)
        "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
 
+syntax (symbols)
+  "op #*"      :: [i, i] => i   (infixr "#\\<times>" 70)
+
+syntax (HTML output)
+  "op #*"      :: [i, i] => i   (infixr "#\\<times>" 70)
+
 rules
   add_def     "a#+b == rec(a, b, %u v. succ(v))"  
   diff_def    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"  
diff -r 78168ca70469 -r e6e7205e9e91 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Tue Nov 14 13:25:59 2000 +0100
+++ b/src/CTT/CTT.thy	Tue Nov 14 13:26:48 2000 +0100
@@ -39,9 +39,9 @@
   eq        :: "i"
   (*Judgements*)
   Type      :: "t => prop"          ("(_ type)" [10] 5)
-  Eqtype    :: "[t,t]=>prop"        ("(3_ =/ _)" [10,10] 5)
+  Eqtype    :: "[t,t]=>prop"        ("(_ =/ _)" [10,10] 5)
   Elem      :: "[i, t]=>prop"       ("(_ /: _)" [10,10] 5)
-  Eqelem    :: "[i,i,t]=>prop"      ("(3_ =/ _ :/ _)" [10,10,10] 5)
+  Eqelem    :: "[i,i,t]=>prop"      ("(_ =/ _ :/ _)" [10,10,10] 5)
   Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
   (*Types*)
   "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
@@ -64,6 +64,17 @@
   "SUM x:A. B"  => "Sum(A, %x. B)"
   "A * B"       => "Sum(A, _K(B))"
 
+syntax (xsymbols)
+  "@-->"    :: "[t,t]=>t"           ("(_ \\<longrightarrow>/ _)" [31,30] 30)
+  "@*"      :: "[t,t]=>t"           ("(_ \\<times>/ _)"          [51,50] 50)
+
+syntax (symbols)
+  Elem      :: "[i, t]=>prop"     ("(_ /\\<in> _)" [10,10] 5)
+  Eqelem    :: "[i,i,t]=>prop"    ("(2_ =/ _ \\<in>/ _)" [10,10,10] 5)
+  "@SUM"    :: "[idt,t,t] => t"   ("(3\\<Sigma> _\\<in>_./ _)" 10)
+  "@PROD"   :: "[idt,t,t] => t"   ("(3\\<Pi> _\\<in>_./ _)"    10)
+  "lam "    :: "[idts, i] => i"   ("(3\\<lambda>\\<lambda>_./ _)" 10)
+
 rules
 
   (*Reduction: a weaker notion than equality;  a hack for simplification.
diff -r 78168ca70469 -r e6e7205e9e91 src/CTT/IsaMakefile
--- a/src/CTT/IsaMakefile	Tue Nov 14 13:25:59 2000 +0100
+++ b/src/CTT/IsaMakefile	Tue Nov 14 13:26:48 2000 +0100
@@ -27,7 +27,7 @@
 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
 $(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.ML Arith.thy \
-  Bool.ML Bool.thy CTT.ML CTT.thy ROOT.ML rew.ML
+  Bool.ML Bool.thy CTT.ML CTT.thy Main.thy ROOT.ML rew.ML
 	@$(ISATOOL) usedir -b $(OUT)/Pure CTT