src/CTT/CTT.thy
 changeset 14765 bafb24c150c1 parent 14565 c6dc17aab88a child 14854 61bdf2ae4dc5
```--- a/src/CTT/CTT.thy	Wed May 19 11:41:58 2004 +0200
+++ b/src/CTT/CTT.thy	Fri May 21 21:14:18 2004 +0200
@@ -34,6 +34,8 @@
split     :: "[i, [i,i]=>i] =>i"
(*General Product and Function Space*)
Prod      :: "[t, i=>t]=>t"
+  (*Types*)
+  "+"       :: "[t,t]=>t"           (infixr 40)
(*Equality type*)
Eq        :: "[t,i,i]=>t"
eq        :: "i"
@@ -44,12 +46,7 @@
Eqelem    :: "[i,i,t]=>prop"      ("(_ =/ _ :/ _)" [10,10,10] 5)
Reduce    :: "[i,i]=>prop"        ("Reduce[_,_]")
(*Types*)
-  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
-  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
-  "+"       :: "[t,t]=>t"           (infixr 40)
-  (*Invisible infixes!*)
-  "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
-  "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
+
(*Functions*)
lambda    :: "(i => i) => i"      (binder "lam " 10)
"`"       :: "[i,i]=>i"           (infixl 60)
@@ -58,6 +55,12 @@
(*Pairing*)
pair      :: "[i,i]=>i"           ("(1<_,/_>)")

+syntax
+  "@PROD"   :: "[idt,t,t]=>t"       ("(3PROD _:_./ _)" 10)
+  "@SUM"    :: "[idt,t,t]=>t"       ("(3SUM _:_./ _)" 10)
+  "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
+  "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
+
translations
"PROD x:A. B" => "Prod(A, %x. B)"
"A --> B"     => "Prod(A, _K(B))"```