src/ZF/ex/PropLog.thy

 
 PropLog = Finite + Datatype +
 
 (** The datatype of propositions; note mixfix syntax **)
 consts
-  prop     :: "i"
+  prop     :: i
 
 datatype
   "prop" = Fls
          | Var ("n: nat")	                ("#_" [100] 100)
          | "=>" ("p: prop", "q: prop")		(infixr 90)
 
 (** The proof system **)
 consts
-  thms     :: "i => i"
-  "|-"     :: "[i,i] => o"    			(infixl 50)
+  thms     :: i => i
+  "|-"     :: [i,i] => o    			(infixl 50)
 
 translations
   "H |- p" == "p : thms(H)"
 
 inductive

   type_intrs "prop.intrs"
 
 
 (** The semantics **)
 consts
-  prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
-  is_true  :: "[i,i] => o"
-  "|="     :: "[i,i] => o"    			(infixl 50)
-  hyps     :: "[i,i] => i"
+  prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
+  is_true  :: [i,i] => o
+  "|="     :: [i,i] => o    			(infixl 50)
+  hyps     :: [i,i] => i
 
 defs
 
   prop_rec_def
    "prop_rec(p,b,c,h) ==