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))"