# HG changeset patch
# User clasohm
# Date 818512571 -3600
# Node ID 0c439768f45ced7f95f065d7b15082cad659aedd
# Parent  5d909faf0e04320fa8d48f49cb8cb50d2bdaab93
removed quotes from consts and syntax sections

diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/AC16_WO4.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -7,11 +7,11 @@
 
 consts
 
-  ww  :: "[i, i] => i"
-  s_u :: "[i, i, i, i] => i"
-  MM  :: "[i, i, i] => i"
-  LL  :: "[i, i, i] => i"
-  GG  :: "[i, i, i] => i"
+  ww  :: [i, i] => i
+  s_u :: [i, i, i, i] => i
+  MM  :: [i, i, i] => i
+  LL  :: [i, i, i] => i
+  GG  :: [i, i, i] => i
   
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/AC18_AC19.thy
--- a/src/ZF/AC/AC18_AC19.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/AC18_AC19.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
 AC18_AC19 = AC_Equiv +
 
 consts
-  u_    :: "i => i"
+  u_    :: i => i
   
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -17,19 +17,19 @@
 consts
   
 (* Well Ordering Theorems *)
-  WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: "o"
-  WO4                               :: "i => o"
+  WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: o
+  WO4                               :: i => o
 
 (* Axioms of Choice *)  
   AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9,
-  AC11, AC12, AC14, AC15, AC17, AC19 :: "o"
-  AC10, AC13              :: "i => o"
-  AC16                    :: "[i, i] => o"
-  AC18                    :: "prop"       ("AC18")
+  AC11, AC12, AC14, AC15, AC17, AC19 :: o
+  AC10, AC13              :: i => o
+  AC16                    :: [i, i] => o
+  AC18                    :: prop       ("AC18")
 
 (* Auxiliary definitions used in definitions *)
-  pairwise_disjoint       :: "i => o"
-  sets_of_size_between    :: "[i, i, i] => o"
+  pairwise_disjoint       :: i => o
+  sets_of_size_between    :: [i, i, i] => o
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/DC.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,9 +9,9 @@
 
 consts
 
-  DC  :: "i => o"
-  DC0 :: "o"
-  ff  :: "[i, i, i, i] => i"
+  DC  :: i => o
+  DC0 :: o
+  ff  :: [i, i, i, i] => i
 
 rules
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/HH.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -12,7 +12,7 @@
 
 consts
  
-  HH                      :: "[i, i, i] => i"
+  HH                      :: [i, i, i] => i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/Hartog.thy
--- a/src/ZF/AC/Hartog.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/Hartog.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
 
 consts
 
-  Hartog :: "i => i"
+  Hartog :: i => i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/OrdQuant.thy
--- a/src/ZF/AC/OrdQuant.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/OrdQuant.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,16 +10,16 @@
 consts
   
   (* Ordinal Quantifiers *)
-  oall, oex   :: "[i, i => o] => o"
+  oall, oex   :: [i, i => o] => o
 
   (* Ordinal Union *)
-  OUnion      :: "[i, i => i] => i"
+  OUnion      :: [i, i => i] => i
   
 syntax
   
-  "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
-  "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
-  "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
+  "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
+  "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
+  "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
 
 translations
   
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/Transrec2.thy
--- a/src/ZF/AC/Transrec2.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/Transrec2.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,7 +10,7 @@
 
 consts
   
-  transrec2               :: "[i, i, [i,i]=>i] =>i"
+  transrec2               :: [i, i, [i,i]=>i] =>i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/WO6_WO1.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -12,10 +12,10 @@
 
 consts
 (* Auxiliary definitions used in proof *)
-  NN            :: "i => i"
-  uu            :: "[i, i, i, i] => i"
-  vv1, ww1, gg1 :: "[i, i, i] => i"
-  vv2, ww2, gg2 :: "[i, i, i, i] => i"
+  NN            :: i => i
+  uu            :: [i, i, i, i] => i
+  vv1, ww1, gg1 :: [i, i, i] => i
+  vv2, ww2, gg2 :: [i, i, i, i] => i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/first.thy
--- a/src/ZF/AC/first.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/first.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
 
 consts
 
-  first                   :: "[i, i, i] => o"
+  first                   :: [i, i, i] => o
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/AC/recfunAC16.thy
--- a/src/ZF/AC/recfunAC16.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/AC/recfunAC16.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
 
 consts
 
-  recfunAC16              :: "[i, i, i, i] => i"
+  recfunAC16              :: [i, i, i, i] => i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Arith.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,12 +8,12 @@
 
 Arith = Epsilon + "simpdata" +
 consts
-    rec  :: "[i, i, [i,i]=>i]=>i"
-    "#*" :: "[i,i]=>i"      		(infixl 70)
-    div  :: "[i,i]=>i"      		(infixl 70) 
-    mod  :: "[i,i]=>i"      		(infixl 70)
-    "#+" :: "[i,i]=>i"      		(infixl 65)
-    "#-" :: "[i,i]=>i"      		(infixl 65)
+    rec  :: [i, i, [i,i]=>i]=>i
+    "#*" :: [i,i]=>i      		(infixl 70)
+    div  :: [i,i]=>i      		(infixl 70) 
+    mod  :: [i,i]=>i      		(infixl 70)
+    "#+" :: [i,i]=>i      		(infixl 65)
+    "#-" :: [i,i]=>i      		(infixl 65)
 
 defs
     rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Bool.thy
--- a/src/ZF/Bool.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Bool.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,14 +10,14 @@
 
 Bool = ZF + "simpdata" +
 consts
-    "1"		:: "i"     	   ("1")
-    "2"         :: "i"             ("2")
-    bool        :: "i"
-    cond        :: "[i,i,i]=>i"
-    not		:: "i=>i"
-    "and"       :: "[i,i]=>i"      (infixl 70)
-    or		:: "[i,i]=>i"      (infixl 65)
-    xor		:: "[i,i]=>i"      (infixl 65)
+    "1"		:: i     	   ("1")
+    "2"         :: i             ("2")
+    bool        :: i
+    cond        :: [i,i,i]=>i
+    not		:: i=>i
+    "and"       :: [i,i]=>i      (infixl 70)
+    or		:: [i,i]=>i      (infixl 65)
+    xor		:: [i,i]=>i      (infixl 65)
 
 translations
    "1"  == "succ(0)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Cardinal.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,11 +8,11 @@
 
 Cardinal = OrderType + Fixedpt + Nat + Sum + 
 consts
-  Least            :: "(i=>o) => i"    (binder "LEAST " 10)
+  Least            :: (i=>o) => i    (binder "LEAST " 10)
   eqpoll, lepoll,
-          lesspoll :: "[i,i] => o"     (infixl 50)
-  cardinal         :: "i=>i"           ("|_|")
-  Finite, Card     :: "i=>o"
+          lesspoll :: [i,i] => o     (infixl 50)
+  cardinal         :: i=>i           ("|_|")
+  Finite, Card     :: i=>o
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/CardinalArith.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,12 +9,12 @@
 CardinalArith = Cardinal + OrderArith + Arith + Finite + 
 consts
 
-  InfCard       :: "i=>o"
-  "|*|"         :: "[i,i]=>i"       (infixl 70)
-  "|+|"         :: "[i,i]=>i"       (infixl 65)
-  csquare_rel   :: "i=>i"
-  jump_cardinal :: "i=>i"
-  csucc         :: "i=>i"
+  InfCard       :: i=>o
+  "|*|"         :: [i,i]=>i       (infixl 70)
+  "|+|"         :: [i,i]=>i       (infixl 65)
+  csquare_rel   :: i=>i
+  jump_cardinal :: i=>i
+  csucc         :: i=>i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/BCR.thy
--- a/src/ZF/Coind/BCR.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/BCR.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,14 +10,14 @@
   parameter of the proof.  A concrete version could be defined inductively.*)
 
 consts
-  isof :: "[i,i] => o"
+  isof :: [i,i] => o
 rules
   isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
 
 (*Its extension to environments*)
 
 consts
-  isofenv :: "[i,i] => o"
+  isofenv :: [i,i] => o
 defs
   isofenv_def "isofenv(ve,te) ==   		
    ve_dom(ve) = te_dom(te) &   		
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/Dynamic.thy
--- a/src/ZF/Coind/Dynamic.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Dynamic.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -7,7 +7,7 @@
 Dynamic = Values +
 
 consts
-  EvalRel :: "i"
+  EvalRel :: i
 inductive
   domains "EvalRel" <= "ValEnv * Exp * Val"
   intrs
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/ECR.thy
--- a/src/ZF/Coind/ECR.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/ECR.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
 (* The extended correspondence relation *)
 
 consts
-  HasTyRel :: "i"
+  HasTyRel :: i
 coinductive
   domains "HasTyRel" <= "Val * Ty"
   intrs
@@ -28,7 +28,7 @@
 (* Pointwise extension to environments *)
  
 consts
-  hastyenv :: "[i,i] => o"
+  hastyenv :: [i,i] => o
 defs
   hastyenv_def 
     " hastyenv(ve,te) == 			
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Language.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -7,8 +7,8 @@
 Language ="Datatype" + QUniv +
 
 consts
-  Const :: "i"			(* Abstract type of constants *)
-  c_app :: "[i,i] => i"		(*Abstract constructor for fun application*)
+  Const :: i			(* Abstract type of constants *)
+  c_app :: [i,i] => i		(*Abstract constructor for fun application*)
 
 rules
   constNEE  "c:Const ==> c ~= 0"
@@ -16,8 +16,8 @@
 
 
 consts
-  Exp   :: "i"			(* Datatype of expressions *)
-  ExVar :: "i"			(* Abstract type of variables *)
+  Exp   :: i			(* Datatype of expressions *)
+  ExVar :: i			(* Abstract type of variables *)
 datatype <= "univ(Const Un ExVar)"
   "Exp" = e_const("c:Const")
         | e_var("x:ExVar")
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Map.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -7,8 +7,8 @@
 Map = QUniv +
 
 consts
-  TMap :: "[i,i] => i"
-  PMap :: "[i,i] => i"
+  TMap :: [i,i] => i
+  PMap :: [i,i] => i
 defs
   TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
   PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
@@ -16,9 +16,9 @@
 (* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
   
 consts
-  map_emp :: "i"
-  map_owr :: "[i,i,i]=>i"
-  map_app :: "[i,i]=>i"
+  map_emp :: i
+  map_owr :: [i,i,i]=>i
+  map_app :: [i,i]=>i
 defs
   map_emp_def "map_emp == 0"
   map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/Static.thy
--- a/src/ZF/Coind/Static.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Static.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -7,7 +7,7 @@
 Static = BCR +
 
 consts
-  ElabRel :: "i"
+  ElabRel :: i
 inductive
   domains "ElabRel" <= "TyEnv * Exp * Ty"
   intrs
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/Types.thy
--- a/src/ZF/Coind/Types.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Types.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -7,8 +7,8 @@
 Types = Language +
 
 consts
-  Ty :: "i"			(* Datatype of types *)
-  TyConst :: "i"		(* Abstract type of type constants *)
+  Ty :: i			(* Datatype of types *)
+  TyConst :: i		(* Abstract type of type constants *)
 datatype <= "univ(TyConst)"
   "Ty" = t_const("tc:TyConst")
        | t_fun("t1:Ty","t2:Ty")
@@ -17,21 +17,21 @@
 (* Definition of type environments and associated operators *)
 
 consts
-  TyEnv :: "i"
+  TyEnv :: i
 datatype <= "univ(Ty Un ExVar)"
   "TyEnv" = te_emp
           | te_owr("te:TyEnv","x:ExVar","t:Ty") 
 
 consts
-  te_rec :: "[i,i,[i,i,i,i]=>i] => i"
+  te_rec :: [i,i,[i,i,i,i]=>i] => i
 defs
   te_rec_def
     "te_rec(te,c,h) ==   
     Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
   
 consts
-  te_dom :: "i => i"
-  te_app :: "[i,i] => i"
+  te_dom :: i => i
+  te_app :: [i,i] => i
 defs
   te_dom_def "te_dom(te) == te_rec(te,0,% te x t r.r Un {x})"
   te_app_def "te_app(te,x) == te_rec(te,0, % te y t r.if(x=y,t,r))"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Coind/Values.thy
--- a/src/ZF/Coind/Values.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Coind/Values.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
 (* Values, values environments and associated operators *)
 
 consts
-  Val, ValEnv, Val_ValEnv  :: "i"
+  Val, ValEnv, Val_ValEnv  :: i
 codatatype <= "quniv(Const Un ExVar Un Exp)"
     "Val" = v_const("c:Const")
           | v_clos("x:ExVar","e:Exp","ve:ValEnv")
@@ -19,10 +19,10 @@
   type_intrs "[A_into_univ, mapQU]"
 
 consts
-  ve_emp :: "i"
-  ve_owr :: "[i,i,i] => i"
-  ve_dom :: "i=>i"
-  ve_app :: "[i,i] => i"
+  ve_emp :: i
+  ve_owr :: [i,i,i] => i
+  ve_dom :: i=>i
+  ve_app :: [i,i] => i
 defs
   ve_emp_def "ve_emp == ve_mk(map_emp)"
   ve_owr_def
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Epsilon.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 Epsilon = Nat + "mono" +
 consts
-    eclose,rank ::      "i=>i"
-    transrec    ::      "[i, [i,i]=>i] =>i"
+    eclose,rank ::      i=>i
+    transrec    ::      [i, [i,i]=>i] =>i
 
 defs
   eclose_def	"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/EquivClass.thy
--- a/src/ZF/EquivClass.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/EquivClass.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
 
 EquivClass = Rel + Perm + 
 consts
-    "'/"        ::      "[i,i]=>i"  (infixl 90)  (*set of equiv classes*)
-    congruent	::	"[i,i=>i]=>o"
-    congruent2  ::      "[i,[i,i]=>i]=>o"
+    "'/"        ::      [i,i]=>i  (infixl 90)  (*set of equiv classes*)
+    congruent	::	[i,i=>i]=>o
+    congruent2  ::      [i,[i,i]=>i]=>o
 
 defs
     quotient_def  "A/r == {r``{x} . x:A}"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Finite.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 Finite = Arith + Inductive +
 consts
-  Fin 	    :: "i=>i"
-  FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
+  Fin 	    :: i=>i
+  FiniteFun :: [i,i]=>i		("(_ -||>/ _)" [61, 60] 60)
 
 inductive
   domains   "Fin(A)" <= "Pow(A)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Fixedpt.thy
--- a/src/ZF/Fixedpt.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Fixedpt.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 Fixedpt = ZF + "domrange" +
 consts
-  bnd_mono    :: "[i,i=>i]=>o"
-  lfp, gfp    :: "[i,i=>i]=>i"
+  bnd_mono    :: [i,i=>i]=>o
+  lfp, gfp    :: [i,i=>i]=>i
 
 defs
   (*monotone operator from Pow(D) to itself*)
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/IMP/Com.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -11,8 +11,8 @@
 Com = Datatype +
 
 (** Arithmetic expressions **)
-consts  loc  :: "i"
-        aexp :: "i"
+consts  loc  :: i
+        aexp :: i
 
 datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
   "aexp" = N ("n: nat")
@@ -22,8 +22,8 @@
 
 
 (** Evaluation of arithmetic expressions **)
-consts  evala    :: "i"
-       "@evala"  :: "[i,i,i] => o"		("<_,_>/ -a-> _"  [0,0,50] 50)
+consts  evala    :: i
+       "@evala"  :: [i,i,i] => o		("<_,_>/ -a-> _"  [0,0,50] 50)
 translations
     "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
 inductive
@@ -39,7 +39,7 @@
 
 
 (** Boolean expressions **)
-consts  bexp :: "i"
+consts  bexp :: i
 
 datatype <= "univ(aexp Un ((nat*nat)->bool) )"
   "bexp" = true
@@ -51,8 +51,8 @@
 
 
 (** Evaluation of boolean expressions **)
-consts evalb	:: "i"	
-       "@evalb" :: "[i,i,i] => o"		("<_,_>/ -b-> _" [0,0,50] 50)
+consts evalb	:: i	
+       "@evalb" :: [i,i,i] => o		("<_,_>/ -b-> _" [0,0,50] 50)
 
 translations
     "<be,sig> -b-> b" == "<be,sig,b> : evalb"
@@ -76,7 +76,7 @@
 
 
 (** Commands **)
-consts  com :: "i"
+consts  com :: i
 
 datatype <= "univ(loc Un aexp Un bexp)"
   "com" = skip
@@ -89,9 +89,9 @@
   with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)
 
 (** Execution of commands **)
-consts  evalc    :: "i"
-        "@evalc" :: "[i,i,i] => o"   		("<_,_>/ -c-> _" [0,0,50] 50)
-	"assign" :: "[i,i,i] => i"   		("_[_'/_]"       [95,0,0] 95)
+consts  evalc    :: i
+        "@evalc" :: [i,i,i] => o   		("<_,_>/ -c-> _" [0,0,50] 50)
+	"assign" :: [i,i,i] => i   		("_[_'/_]"       [95,0,0] 95)
 
 translations
        "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/IMP/Denotation.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,10 +9,10 @@
 Denotation = Com + 
 
 consts
-  A     :: "i => i => i"
-  B     :: "i => i => i"
-  C     :: "i => i"
-  Gamma :: "[i,i,i] => i"
+  A     :: i => i => i
+  B     :: i => i => i
+  C     :: i => i
+  Gamma :: [i,i,i] => i
 
 rules	(*NOT definitional*)
   A_nat_def	"A(N(n)) == (%sigma. n)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Let.thy
--- a/src/ZF/Let.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Let.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -12,13 +12,13 @@
   letbinds  letbind
 
 consts
-  Let           :: "['a, 'a => 'b] => 'b"
+  Let           :: ['a, 'a => 'b] => 'b
 
 syntax
-  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
-  ""            :: "letbind => letbinds"              ("_")
-  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
-  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
+  "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
+  ""            :: letbind => letbinds              ("_")
+  "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
+  "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
 
 translations
   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/List.thy
--- a/src/ZF/List.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/List.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -13,20 +13,20 @@
 List = Datatype + 
 
 consts
-  "@"	     :: "[i,i]=>i"      			(infixr 60)
-  list_rec   :: "[i, i, [i,i,i]=>i] => i"
-  map 	     :: "[i=>i, i] => i"
-  length,rev :: "i=>i"
-  flat       :: "i=>i"
-  list_add   :: "i=>i"
-  hd,tl      :: "i=>i"
-  drop	     :: "[i,i]=>i"
+  "@"	     :: [i,i]=>i      			(infixr 60)
+  list_rec   :: [i, i, [i,i,i]=>i] => i
+  map 	     :: [i=>i, i] => i
+  length,rev :: i=>i
+  flat       :: i=>i
+  list_add   :: i=>i
+  hd,tl      :: i=>i
+  drop	     :: [i,i]=>i
 
  (* List Enumeration *)
- "[]"        :: "i" 	                           	("[]")
- "@List"     :: "is => i" 	                   	("[(_)]")
+ "[]"        :: i 	                           	("[]")
+ "@List"     :: is => i 	                   	("[(_)]")
 
-  list	     :: "i=>i"
+  list	     :: i=>i
 
   
 datatype
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Nat.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
 
 Nat = Ordinal + Bool + "mono" +
 consts
-    nat 	::      "i"
-    nat_case    ::      "[i, i=>i, i]=>i"
-    nat_rec     ::      "[i, i, [i,i]=>i]=>i"
+    nat 	::      i
+    nat_case    ::      [i, i=>i, i]=>i
+    nat_rec     ::      [i, i, [i,i]=>i]=>i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Order.thy
--- a/src/ZF/Order.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Order.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,13 +8,13 @@
 
 Order = WF + Perm + 
 consts
-  part_ord        :: "[i,i]=>o"		(*Strict partial ordering*)
-  linear, tot_ord :: "[i,i]=>o"		(*Strict total ordering*)
-  well_ord        :: "[i,i]=>o"		(*Well-ordering*)
-  mono_map        :: "[i,i,i,i]=>i"	(*Order-preserving maps*)
-  ord_iso         :: "[i,i,i,i]=>i"	(*Order isomorphisms*)
-  pred            :: "[i,i,i]=>i"	(*Set of predecessors*)
-  ord_iso_map     :: "[i,i,i,i]=>i"	(*Construction for linearity theorem*)
+  part_ord        :: [i,i]=>o		(*Strict partial ordering*)
+  linear, tot_ord :: [i,i]=>o		(*Strict total ordering*)
+  well_ord        :: [i,i]=>o		(*Well-ordering*)
+  mono_map        :: [i,i,i,i]=>i	(*Order-preserving maps*)
+  ord_iso         :: [i,i,i,i]=>i	(*Order isomorphisms*)
+  pred            :: [i,i,i]=>i	(*Set of predecessors*)
+  ord_iso_map     :: [i,i,i,i]=>i	(*Construction for linearity theorem*)
 
 defs
   part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/OrderArith.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 OrderArith = Order + Sum + 
 consts
-  radd, rmult      :: "[i,i,i,i]=>i"
-  rvimage          :: "[i,i,i]=>i"
+  radd, rmult      :: [i,i,i,i]=>i
+  rvimage          :: [i,i,i]=>i
 
 defs
   (*disjoint sum of two relations; underlies ordinal addition*)
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/OrderType.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,14 +10,14 @@
 
 OrderType = OrderArith + Ordinal + 
 consts
-  ordermap  :: "[i,i]=>i"
-  ordertype :: "[i,i]=>i"
+  ordermap  :: [i,i]=>i
+  ordertype :: [i,i]=>i
 
-  Ord_alt   :: "i => o"   
+  Ord_alt   :: i => o   
 
-  "**"      :: "[i,i]=>i"           (infixl 70)
-  "++"      :: "[i,i]=>i"           (infixl 65)
-  "--"      :: "[i,i]=>i"           (infixl 65)
+  "**"      :: [i,i]=>i           (infixl 70)
+  "++"      :: [i,i]=>i           (infixl 65)
+  "--"      :: [i,i]=>i           (infixl 65)
  
 
 defs
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Ordinal.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,11 +8,11 @@
 
 Ordinal = WF + Bool + "simpdata" + "equalities" +
 consts
-  Memrel      	:: "i=>i"
-  Transset,Ord  :: "i=>o"
-  "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
-  "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
-  Limit         :: "i=>o"
+  Memrel      	:: i=>i
+  Transset,Ord  :: i=>o
+  "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
+  "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
+  Limit         :: i=>o
 
 translations
   "x le y"      == "x < succ(y)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Perm.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -11,9 +11,9 @@
 
 Perm = ZF + "mono" +
 consts
-    O    	::      "[i,i]=>i"      (infixr 60)
-    id  	::      "i=>i"
-    inj,surj,bij::      "[i,i]=>i"
+    O    	::      [i,i]=>i      (infixr 60)
+    id  	::      i=>i
+    inj,surj,bij::      [i,i]=>i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/QPair.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -13,19 +13,19 @@
 
 QPair = Sum + "simpdata" +
 consts
-  QPair     :: "[i, i] => i"               	("<(_;/ _)>")
-  qfst,qsnd :: "i => i"
-  qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
-  qconverse :: "i => i"
-  QSigma    :: "[i, i => i] => i"
+  QPair     :: [i, i] => i               	("<(_;/ _)>")
+  qfst,qsnd :: i => i
+  qsplit    :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
+  qconverse :: i => i
+  QSigma    :: [i, i => i] => i
 
-  "<+>"     :: "[i,i]=>i"      			(infixr 65)
-  QInl,QInr :: "i=>i"
-  qcase     :: "[i=>i, i=>i, i]=>i"
+  "<+>"     :: [i,i]=>i      			(infixr 65)
+  QInl,QInr :: i=>i
+  qcase     :: [i=>i, i=>i, i]=>i
 
 syntax
-  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
-  "<*>"     :: "[i, i] => i"         		(infixr 80)
+  "@QSUM"   :: [idt, i, i] => i               ("(3QSUM _:_./ _)" 10)
+  "<*>"     :: [i, i] => i         		(infixr 80)
 
 translations
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/QUniv.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,7 +8,7 @@
 
 QUniv = Univ + QPair + "mono" + "equalities" +
 consts
-    quniv        :: "i=>i"
+    quniv        :: i=>i
 
 defs
     quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Rel.thy
--- a/src/ZF/Rel.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Rel.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
 
 Rel = ZF +
 consts
-    refl,irrefl,equiv      :: "[i,i]=>o"
-    sym,asym,antisym,trans :: "i=>o"
-    trans_on               :: "[i,i]=>o"	("trans[_]'(_')")
+    refl,irrefl,equiv      :: [i,i]=>o
+    sym,asym,antisym,trans :: i=>o
+    trans_on               :: [i,i]=>o	("trans[_]'(_')")
 
 defs
   refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/Confluence.thy
--- a/src/ZF/Resid/Confluence.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Confluence.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 Confluence = Reduction+
 
 consts
-  confluence	:: "i=>o"
-  strip		:: "o"
+  confluence	:: i=>o
+  strip		:: o
 
 defs
   confluence_def "confluence(R) ==   
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/Conversion.thy
--- a/src/ZF/Resid/Conversion.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Conversion.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,10 +9,10 @@
 Conversion = Confluence+
 
 consts
-  Sconv1	:: "i"
-  "<-1->"	:: "[i,i]=>o" (infixl 50)
-  Sconv		:: "i"
-  "<--->"	:: "[i,i]=>o" (infixl 50)
+  Sconv1	:: i
+  "<-1->"	:: [i,i]=>o (infixl 50)
+  Sconv		:: i
+  "<--->"	:: [i,i]=>o (infixl 50)
 
 translations
   "a<-1->b"    == "<a,b>:Sconv1"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Redex.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -7,7 +7,7 @@
 
 Redex = Univ +
 consts
-  redexes     :: "i"
+  redexes     :: i
 
 datatype
   "redexes" = Var ("n: nat")	        
@@ -17,7 +17,7 @@
   
 
 consts
-  redex_rec   	:: "[i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i"
+  redex_rec   	:: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
  
 defs
   redex_rec_def
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Reduction.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 Reduction = Terms+
 
 consts
-  Sred1, Sred,  Spar_red1,Spar_red    :: "i"
-  "-1->","--->","=1=>",   "===>"      :: "[i,i]=>o" (infixl 50)
+  Sred1, Sred,  Spar_red1,Spar_red    :: i
+  "-1->","--->","=1=>",   "===>"      :: [i,i]=>o (infixl 50)
 
 translations
   "a -1-> b" == "<a,b>:Sred1"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Residuals.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,9 +9,9 @@
 Residuals = Substitution+
 
 consts
-  Sres		:: "i"
-  residuals	:: "[i,i,i]=>i"
-  "|>"		:: "[i,i]=>i"     (infixl 70)
+  Sres		:: i
+  residuals	:: [i,i,i]=>i
+  "|>"		:: [i,i]=>i     (infixl 70)
   
 translations
   "residuals(u,v,w)"  == "<u,v,w>:Sres"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/SubUnion.thy
--- a/src/ZF/Resid/SubUnion.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/SubUnion.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,10 +8,10 @@
 SubUnion = Redex +
 
 consts
-  Ssub,Scomp,Sreg  :: "i"
-  "<==","~"        :: "[i,i]=>o" (infixl 70)
-  un               :: "[i,i]=>i" (infixl 70)
-  regular	   :: "i=>o"
+  Ssub,Scomp,Sreg  :: i
+  "<==","~"        :: [i,i]=>o (infixl 70)
+  un               :: [i,i]=>i (infixl 70)
+  regular	   :: i=>o
   
 translations
   "a<==b"        == "<a,b>:Ssub"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Substitution.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,10 +8,10 @@
 Substitution = SubUnion +
 
 consts
-  lift_rec	:: "[i,i]=> i"
-  lift		:: "i=>i"
-  subst_rec	:: "[i,i,i]=> i"
-  "'/"          :: "[i,i]=>i"  (infixl 70)  (*subst*)
+  lift_rec	:: [i,i]=> i
+  lift		:: i=>i
+  subst_rec	:: [i,i,i]=> i
+  "'/"          :: [i,i]=>i  (infixl 70)  (*subst*)
 translations
   "lift(r)"  == "lift_rec(r,0)"
   "u/v" == "subst_rec(u,v,0)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Resid/Terms.thy
--- a/src/ZF/Resid/Terms.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Resid/Terms.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,9 +8,9 @@
 Terms = Cube+
 
 consts
-  lambda	:: "i"
-  unmark	:: "i=>i"
-  Apl		:: "[i,i]=>i"
+  lambda	:: i
+  unmark	:: i=>i
+  Apl		:: [i,i]=>i
 
 translations
   "Apl(n,m)" == "App(0,n,m)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Sum.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,10 +9,10 @@
 
 Sum = Bool + "simpdata" +
 consts
-    "+"    	:: "[i,i]=>i"      		(infixr 65)
-    Inl,Inr     :: "i=>i"
-    case        :: "[i=>i, i=>i, i]=>i"
-    Part        :: "[i,i=>i] => i"
+    "+"    	:: [i,i]=>i      		(infixr 65)
+    Inl,Inr     :: i=>i
+    case        :: [i=>i, i=>i, i]=>i
+    Part        :: [i,i=>i] => i
 
 defs
     sum_def     "A+B == {0}*A Un {1}*B"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Trancl.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 Trancl = Fixedpt + Perm + "mono" + Rel + 
 consts
-    rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
-    trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
+    rtrancl :: i=>i  ("(_^*)" [100] 100)  (*refl/transitive closure*)
+    trancl  :: i=>i  ("(_^+)" [100] 100)  (*transitive closure*)
 
 defs
     rtrancl_def	"r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Univ.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -13,10 +13,10 @@
 
 Univ = Arith + Sum + Finite + "mono" +
 consts
-    Vfrom       :: "[i,i]=>i"
-    Vset        :: "i=>i"
-    Vrec        :: "[i, [i,i]=>i] =>i"
-    univ        :: "i=>i"
+    Vfrom       :: [i,i]=>i
+    Vset        :: i=>i
+    Vrec        :: [i, [i,i]=>i] =>i
+    univ        :: i=>i
 
 translations
     "Vset(x)"   == 	"Vfrom(0,x)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/WF.thy
--- a/src/ZF/WF.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/WF.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,13 +8,13 @@
 
 WF = Trancl + "mono" + "equalities" +
 consts
-  wf           :: "i=>o"
-  wf_on        :: "[i,i]=>o"			("wf[_]'(_')")
+  wf           :: i=>o
+  wf_on        :: [i,i]=>o			("wf[_]'(_')")
 
-  wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"
-  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"	("wfrec[_]'(_,_,_')")
-  is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
-  the_recfun   :: "[i, i, [i,i]=>i] =>i"
+  wftrec,wfrec :: [i, i, [i,i]=>i] =>i
+  wfrec_on     :: [i, i, i, [i,i]=>i] =>i	("wfrec[_]'(_,_,_')")
+  is_recfun    :: [i, i, [i,i]=>i, i] =>o
+  the_recfun   :: [i, i, [i,i]=>i] =>i
 
 defs
   (*r is a well-founded relation*)
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ZF.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -16,68 +16,68 @@
 
 consts
 
-  "0"         :: "i"                  ("0")   (*the empty set*)
-  Pow         :: "i => i"                     (*power sets*)
-  Inf         :: "i"                          (*infinite set*)
+  "0"         :: i                  ("0")   (*the empty set*)
+  Pow         :: i => i                     (*power sets*)
+  Inf         :: i                          (*infinite set*)
 
   (* Bounded Quantifiers *)
 
-  Ball, Bex   :: "[i, i => o] => o"
+  Ball, Bex   :: [i, i => o] => o
 
   (* General Union and Intersection *)
 
-  Union,Inter :: "i => i"
+  Union,Inter :: i => i
 
   (* Variations on Replacement *)
 
-  PrimReplace :: "[i, [i, i] => o] => i"
-  Replace     :: "[i, [i, i] => o] => i"
-  RepFun      :: "[i, i => i] => i"
-  Collect     :: "[i, i => o] => i"
+  PrimReplace :: [i, [i, i] => o] => i
+  Replace     :: [i, [i, i] => o] => i
+  RepFun      :: [i, i => i] => i
+  Collect     :: [i, i => o] => i
 
   (* Descriptions *)
 
-  The         :: "(i => o) => i"      (binder "THE " 10)
-  if          :: "[o, i, i] => i"
+  The         :: (i => o) => i      (binder "THE " 10)
+  if          :: [o, i, i] => i
 
   (* Finite Sets *)
 
-  Upair, cons :: "[i, i] => i"
-  succ        :: "i => i"
+  Upair, cons :: [i, i] => i
+  succ        :: i => i
 
   (* Ordered Pairing *)
 
-  Pair        :: "[i, i] => i"
-  fst, snd    :: "i => i"
-  split       :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
+  Pair        :: [i, i] => i
+  fst, snd    :: i => i
+  split       :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
 
   (* Sigma and Pi Operators *)
 
-  Sigma, Pi   :: "[i, i => i] => i"
+  Sigma, Pi   :: [i, i => i] => i
 
   (* Relations and Functions *)
 
-  domain      :: "i => i"
-  range       :: "i => i"
-  field       :: "i => i"
-  converse    :: "i => i"
-  function    :: "i => o"	    	(*is a relation a function?*)
-  Lambda      :: "[i, i => i] => i"
-  restrict    :: "[i, i] => i"
+  domain      :: i => i
+  range       :: i => i
+  field       :: i => i
+  converse    :: i => i
+  function    :: i => o	    	(*is a relation a function?*)
+  Lambda      :: [i, i => i] => i
+  restrict    :: [i, i] => i
 
   (* Infixes in order of decreasing precedence *)
 
-  "``"        :: "[i, i] => i"    (infixl 90) (*image*)
-  "-``"       :: "[i, i] => i"    (infixl 90) (*inverse image*)
-  "`"         :: "[i, i] => i"    (infixl 90) (*function application*)
-(*"*"         :: "[i, i] => i"    (infixr 80) (*Cartesian product*)*)
-  "Int"       :: "[i, i] => i"    (infixl 70) (*binary intersection*)
-  "Un"        :: "[i, i] => i"    (infixl 65) (*binary union*)
-  "-"         :: "[i, i] => i"    (infixl 65) (*set difference*)
-(*"->"        :: "[i, i] => i"    (infixr 60) (*function space*)*)
-  "<="        :: "[i, i] => o"    (infixl 50) (*subset relation*)
-  ":"         :: "[i, i] => o"    (infixl 50) (*membership relation*)
-(*"~:"        :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
+  "``"        :: [i, i] => i    (infixl 90) (*image*)
+  "-``"       :: [i, i] => i    (infixl 90) (*inverse image*)
+  "`"         :: [i, i] => i    (infixl 90) (*function application*)
+(*"*"         :: [i, i] => i    (infixr 80) (*Cartesian product*)*)
+  "Int"       :: [i, i] => i    (infixl 70) (*binary intersection*)
+  "Un"        :: [i, i] => i    (infixl 65) (*binary union*)
+  "-"         :: [i, i] => i    (infixl 65) (*set difference*)
+(*"->"        :: [i, i] => i    (infixr 60) (*function space*)*)
+  "<="        :: [i, i] => o    (infixl 50) (*subset relation*)
+  ":"         :: [i, i] => o    (infixl 50) (*membership relation*)
+(*"~:"        :: [i, i] => o    (infixl 50) (*negated membership relation*)*)
 
 
 types
@@ -85,29 +85,29 @@
   pttrns
 
 syntax
-  ""          :: "i => is"                   ("_")
-  "@Enum"     :: "[i, is] => is"             ("_,/ _")
-  "~:"        :: "[i, i] => o"               (infixl 50)
-  "@Finset"   :: "is => i"                   ("{(_)}")
-  "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
-  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
-  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
-  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
-  "@INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
-  "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
-  "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
-  "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
-  "->"        :: "[i, i] => i"               (infixr 60)
-  "*"         :: "[i, i] => i"               (infixr 80)
-  "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
-  "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
-  "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
+  ""          :: i => is                   ("_")
+  "@Enum"     :: [i, is] => is             ("_,/ _")
+  "~:"        :: [i, i] => o               (infixl 50)
+  "@Finset"   :: is => i                   ("{(_)}")
+  "@Tuple"    :: [i, is] => i              ("<(_,/ _)>")
+  "@Collect"  :: [pttrn, i, o] => i        ("(1{_: _ ./ _})")
+  "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _: _, _})")
+  "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _: _})" [51,0,51])
+  "@INTER"    :: [pttrn, i, i] => i        ("(3INT _:_./ _)" 10)
+  "@UNION"    :: [pttrn, i, i] => i        ("(3UN _:_./ _)" 10)
+  "@PROD"     :: [pttrn, i, i] => i        ("(3PROD _:_./ _)" 10)
+  "@SUM"      :: [pttrn, i, i] => i        ("(3SUM _:_./ _)" 10)
+  "->"        :: [i, i] => i               (infixr 60)
+  "*"         :: [i, i] => i               (infixr 80)
+  "@lam"      :: [pttrn, i, i] => i        ("(3lam _:_./ _)" 10)
+  "@Ball"     :: [pttrn, i, o] => o        ("(3ALL _:_./ _)" 10)
+  "@Bex"      :: [pttrn, i, o] => o        ("(3EX _:_./ _)" 10)
 
   (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
 
-  "@pttrn"  :: "pttrns => pttrn"            ("<_>")
-  ""        :: " pttrn           => pttrns" ("_")
-  "@pttrns" :: "[pttrn,pttrns]   => pttrns" ("_,/_")
+  "@pttrn"  :: pttrns => pttrn            ("<_>")
+  ""        ::  pttrn           => pttrns ("_")
+  "@pttrns" :: [pttrn,pttrns]   => pttrns ("_,/_")
 
 translations
   "x ~: y"      == "~ (x : y)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Zorn.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -14,10 +14,10 @@
 Zorn = OrderArith + AC + Inductive +
 
 consts
-  Subset_rel      :: "i=>i"
-  increasing      :: "i=>i"
-  chain, maxchain :: "i=>i"
-  super           :: "[i,i]=>i"
+  Subset_rel      :: i=>i
+  increasing      :: i=>i
+  chain, maxchain :: i=>i
+  super           :: [i,i]=>i
 
 defs
   Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
@@ -34,7 +34,7 @@
     are therefore unconditional.
 **)
 consts
-  "TFin" :: "[i,i]=>i"
+  "TFin" :: [i,i]=>i
 
 inductive
   domains       "TFin(S,next)" <= "Pow(S)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Acc.thy
--- a/src/ZF/ex/Acc.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Acc.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -12,7 +12,7 @@
 Acc = WF + Inductive +
 
 consts
-  acc :: "i=>i"
+  acc :: i=>i
 
 inductive
   domains "acc(r)" <= "field(r)"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/BT.thy
--- a/src/ZF/ex/BT.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/BT.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,12 +8,12 @@
 
 BT = Datatype +
 consts
-    bt_rec    	:: "[i, i, [i,i,i,i,i]=>i] => i"
-    n_nodes	:: "i=>i"
-    n_leaves   	:: "i=>i"
-    bt_reflect 	:: "i=>i"
+    bt_rec    	:: [i, i, [i,i,i,i,i]=>i] => i
+    n_nodes	:: i=>i
+    n_leaves   	:: i=>i
+    bt_reflect 	:: i=>i
 
-    bt 	        :: "i=>i"
+    bt 	        :: i=>i
 
 datatype
   "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Bin.thy
--- a/src/ZF/ex/Bin.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Bin.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -21,18 +21,18 @@
 Bin = Integ + Datatype + "twos_compl" +
 
 consts
-  bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
-  integ_of_bin     :: "i=>i"
-  norm_Bcons       :: "[i,i]=>i"
-  bin_succ         :: "i=>i"
-  bin_pred         :: "i=>i"
-  bin_minus        :: "i=>i"
-  bin_add,bin_mult :: "[i,i]=>i"
+  bin_rec          :: [i, i, i, [i,i,i]=>i] => i
+  integ_of_bin     :: i=>i
+  norm_Bcons       :: [i,i]=>i
+  bin_succ         :: i=>i
+  bin_pred         :: i=>i
+  bin_minus        :: i=>i
+  bin_add,bin_mult :: [i,i]=>i
 
-  bin              :: "i"
+  bin              :: i
 
 syntax
-  "_Int"           :: "xnum => i"        ("_")
+  "_Int"           :: xnum => i        ("_")
 
 datatype
   "bin" = Plus
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Brouwer.thy
--- a/src/ZF/ex/Brouwer.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Brouwer.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,8 +10,8 @@
 
 Brouwer = InfDatatype +
 consts
-  brouwer :: "i"
-  Well    :: "[i,i=>i]=>i"
+  brouwer :: i
+  Well    :: [i,i=>i]=>i
  
 datatype <= "Vfrom(0, csucc(nat))"
   "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/CoUnit.thy
--- a/src/ZF/ex/CoUnit.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/CoUnit.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -17,7 +17,7 @@
   Coalgebra Theorem
 *)
 consts
-  counit :: "i"
+  counit :: i
 codatatype
   "counit" = Con ("x: counit")
 
@@ -27,7 +27,7 @@
 *)
 
 consts
-  counit2 :: "i"
+  counit2 :: i
 codatatype
   "counit2" = Con2 ("x: counit2", "y: counit2")
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Comb.thy
--- a/src/ZF/ex/Comb.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Comb.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -16,7 +16,7 @@
 Comb = Datatype +
 
 (** Datatype definition of combinators S and K, with infixed application **)
-consts comb :: "i"
+consts comb :: i
 datatype (* <= "univ(0)" *)
   "comb" = K
          | S
@@ -26,9 +26,9 @@
              and (multi-step) reductions, --->
 **)
 consts
-  contract  :: "i"
-  "-1->"    :: "[i,i] => o"    			(infixl 50)
-  "--->"    :: "[i,i] => o"    			(infixl 50)
+  contract  :: i
+  "-1->"    :: [i,i] => o    			(infixl 50)
+  "--->"    :: [i,i] => o    			(infixl 50)
 
 translations
   "p -1-> q" == "<p,q> : contract"
@@ -48,9 +48,9 @@
              and (multi-step) parallel reductions, ===>
 **)
 consts
-  parcontract :: "i"
-  "=1=>"    :: "[i,i] => o"    			(infixl 50)
-  "===>"    :: "[i,i] => o"    			(infixl 50)
+  parcontract :: i
+  "=1=>"    :: [i,i] => o    			(infixl 50)
+  "===>"    :: [i,i] => o    			(infixl 50)
 
 translations
   "p =1=> q" == "<p,q> : parcontract"
@@ -68,8 +68,8 @@
 
 (*Misc definitions*)
 consts
-  diamond   :: "i => o"
-  I         :: "i"
+  diamond   :: i => o
+  I         :: i
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Data.thy
--- a/src/ZF/ex/Data.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Data.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,7 +10,7 @@
 Data = Datatype +
 
 consts
-  data :: "[i,i] => i"
+  data :: [i,i] => i
 
 datatype
   "data(A,B)" = Con0
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Enum.thy
--- a/src/ZF/ex/Enum.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Enum.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -11,7 +11,7 @@
 Enum = Datatype + 
 
 consts
-  enum :: "i"
+  enum :: i
 
 datatype
   "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Integ.thy
--- a/src/ZF/ex/Integ.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Integ.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,17 +8,17 @@
 
 Integ = EquivClass + Arith +
 consts
-    intrel,integ::      "i"
-    znat	::	"i=>i"		("$# _" [80] 80)
-    zminus	::	"i=>i"		("$~ _" [80] 80)
-    znegative	::	"i=>o"
-    zmagnitude	::	"i=>i"
-    "$*"        ::      "[i,i]=>i"      (infixl 70)
-    "$'/"       ::      "[i,i]=>i"      (infixl 70) 
-    "$'/'/"     ::      "[i,i]=>i"      (infixl 70)
-    "$+"	::      "[i,i]=>i"      (infixl 65)
-    "$-"        ::      "[i,i]=>i"      (infixl 65)
-    "$<"	:: 	"[i,i]=>o"  	(infixl 50)
+    intrel,integ::      i
+    znat	::	i=>i		("$# _" [80] 80)
+    zminus	::	i=>i		("$~ _" [80] 80)
+    znegative	::	i=>o
+    zmagnitude	::	i=>i
+    "$*"        ::      [i,i]=>i      (infixl 70)
+    "$'/"       ::      [i,i]=>i      (infixl 70) 
+    "$'/'/"     ::      [i,i]=>i      (infixl 70)
+    "$+"	::      [i,i]=>i      (infixl 65)
+    "$-"        ::      [i,i]=>i      (infixl 65)
+    "$<"	:: 	[i,i]=>o  	(infixl 50)
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/LList.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -17,7 +17,7 @@
 LList = Datatype +
 
 consts
-  llist  :: "i=>i"
+  llist  :: i=>i
 
 codatatype
   "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
@@ -25,7 +25,7 @@
 
 (*Coinductive definition of equality*)
 consts
-  lleq :: "i=>i"
+  lleq :: i=>i
 
 (*Previously used <*> in the domain and variant pairs as elements.  But
   standard pairs work just as well.  To use variant pairs, must change prefix
@@ -40,8 +40,8 @@
 
 (*Lazy list functions; flip is not definitional!*)
 consts
-  lconst   :: "i => i"
-  flip     :: "i => i"
+  lconst   :: i => i
+  flip     :: i => i
 
 defs
   lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Limit.thy
--- a/src/ZF/ex/Limit.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Limit.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -21,43 +21,43 @@
 
 consts
 
-  "rel" :: "[i,i,i]=>o"                 (* rel(D,x,y) *)
-  "set" :: "i=>i"                       (* set(D) *)
-  "po"  :: "i=>o"                       (* po(D) *)
-  "chain" :: "[i,i]=>o"                 (* chain(D,X) *)
-  "isub" :: "[i,i,i]=>o"                (* isub(D,X,x) *)
-  "islub" :: "[i,i,i]=>o"               (* islub(D,X,x) *)
-  "lub" :: "[i,i]=>i"                   (* lub(D,X) *)
-  "cpo" :: "i=>o"                       (* cpo(D) *)
-  "pcpo" :: "i=>o"                      (* pcpo(D) *)
-  "bot" :: "i=>i"                       (* bot(D) *)
-  "mono" :: "[i,i]=>i"                  (* mono(D,E) *)
-  "cont" :: "[i,i]=>i"                  (* cont(D,E) *)
-  "cf" :: "[i,i]=>i"                    (* cf(D,E) *)
+  "rel" :: [i,i,i]=>o                 (* rel(D,x,y) *)
+  "set" :: i=>i                       (* set(D) *)
+  "po"  :: i=>o                       (* po(D) *)
+  "chain" :: [i,i]=>o                 (* chain(D,X) *)
+  "isub" :: [i,i,i]=>o                (* isub(D,X,x) *)
+  "islub" :: [i,i,i]=>o               (* islub(D,X,x) *)
+  "lub" :: [i,i]=>i                   (* lub(D,X) *)
+  "cpo" :: i=>o                       (* cpo(D) *)
+  "pcpo" :: i=>o                      (* pcpo(D) *)
+  "bot" :: i=>i                       (* bot(D) *)
+  "mono" :: [i,i]=>i                  (* mono(D,E) *)
+  "cont" :: [i,i]=>i                  (* cont(D,E) *)
+  "cf" :: [i,i]=>i                    (* cf(D,E) *)
 
-  "suffix" :: "[i,i]=>i"                (* suffix(X,n) *)
-  "subchain" :: "[i,i]=>o"              (* subchain(X,Y) *)
-  "dominate" :: "[i,i,i]=>o"            (* dominate(D,X,Y) *)
-  "matrix" :: "[i,i]=>o"                (* matrix(D,M) *)
+  "suffix" :: [i,i]=>i                (* suffix(X,n) *)
+  "subchain" :: [i,i]=>o              (* subchain(X,Y) *)
+  "dominate" :: [i,i,i]=>o            (* dominate(D,X,Y) *)
+  "matrix" :: [i,i]=>o                (* matrix(D,M) *)
 
-  "projpair"  :: "[i,i,i,i]=>o"         (* projpair(D,E,e,p) *)
-  "emb"       :: "[i,i,i]=>o"           (* emb(D,E,e) *)
-  "Rp"        :: "[i,i,i]=>i"           (* Rp(D,E,e) *)
-  "iprod"     :: "i=>i"                 (* iprod(DD) *)
-  "mkcpo"     :: "[i,i=>o]=>i"          (* mkcpo(D,P) *)
-  "subcpo"    :: "[i,i]=>o"             (* subcpo(D,E) *)
-  "subpcpo"   :: "[i,i]=>o"             (* subpcpo(D,E) *)
+  "projpair"  :: [i,i,i,i]=>o         (* projpair(D,E,e,p) *)
+  "emb"       :: [i,i,i]=>o           (* emb(D,E,e) *)
+  "Rp"        :: [i,i,i]=>i           (* Rp(D,E,e) *)
+  "iprod"     :: i=>i                 (* iprod(DD) *)
+  "mkcpo"     :: [i,i=>o]=>i          (* mkcpo(D,P) *)
+  "subcpo"    :: [i,i]=>o             (* subcpo(D,E) *)
+  "subpcpo"   :: [i,i]=>o             (* subpcpo(D,E) *)
 
-  "emb_chain" :: "[i,i]=>o"             (* emb_chain(DD,ee) *)
-  "Dinf"      :: "[i,i]=>i"             (* Dinf(DD,ee) *)
+  "emb_chain" :: [i,i]=>o             (* emb_chain(DD,ee) *)
+  "Dinf"      :: [i,i]=>i             (* Dinf(DD,ee) *)
 
-  "e_less"    :: "[i,i,i,i]=>i"         (* e_less(DD,ee,m,n) *)
-  "e_gr"      :: "[i,i,i,i]=>i"         (* e_gr(DD,ee,m,n) *)
-  "eps"       :: "[i,i,i,i]=>i"         (* eps(DD,ee,m,n) *)
-  "rho_emb"   :: "[i,i,i]=>i"           (* rho_emb(DD,ee,n) *)
-  "rho_proj"  :: "[i,i,i]=>i"           (* rho_proj(DD,ee,n) *)
-  "commute"   :: "[i,i,i,i=>i]=>o"      (* commute(DD,ee,E,r) *)
-  "mediating" :: "[i,i,i=>i,i=>i,i]=>o" (* mediating(E,G,r,f,t) *)
+  "e_less"    :: [i,i,i,i]=>i         (* e_less(DD,ee,m,n) *)
+  "e_gr"      :: [i,i,i,i]=>i         (* e_gr(DD,ee,m,n) *)
+  "eps"       :: [i,i,i,i]=>i         (* eps(DD,ee,m,n) *)
+  "rho_emb"   :: [i,i,i]=>i           (* rho_emb(DD,ee,n) *)
+  "rho_proj"  :: [i,i,i]=>i           (* rho_proj(DD,ee,n) *)
+  "commute"   :: [i,i,i,i=>i]=>o      (* commute(DD,ee,E,r) *)
+  "mediating" :: [i,i,i=>i,i=>i,i]=>o (* mediating(E,G,r,f,t) *)
 
 rules
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/ListN.thy
--- a/src/ZF/ex/ListN.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/ListN.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -10,7 +10,7 @@
 *)
 
 ListN = List +
-consts	listn ::"i=>i"
+consts	listn ::i=>i
 inductive
   domains   "listn(A)" <= "nat*list(A)"
   intrs
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Ntree.thy
--- a/src/ZF/ex/Ntree.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Ntree.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -11,9 +11,9 @@
 
 Ntree = InfDatatype +
 consts
-  ntree    :: "i=>i"
-  maptree  :: "i=>i"
-  maptree2 :: "[i,i] => i"
+  ntree    :: i=>i
+  maptree  :: i=>i
+  maptree2 :: [i,i] => i
 
 datatype
   "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Primrec.thy
--- a/src/ZF/ex/Primrec.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Primrec.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -16,14 +16,14 @@
 
 Primrec = List +
 consts
-    primrec :: "i"
-    SC      :: "i"
-    CONST   :: "i=>i"
-    PROJ    :: "i=>i"
-    COMP    :: "[i,i]=>i"
-    PREC    :: "[i,i]=>i"
-    ACK	    :: "i=>i"
-    ack	    :: "[i,i]=>i"
+    primrec :: i
+    SC      :: i
+    CONST   :: i=>i
+    PROJ    :: i=>i
+    COMP    :: [i,i]=>i
+    PREC    :: [i,i]=>i
+    ACK	    :: i=>i
+    ack	    :: [i,i]=>i
 
 translations
   "ack(x,y)"  == "ACK(x) ` [y]"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/PropLog.thy
--- a/src/ZF/ex/PropLog.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/PropLog.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -11,7 +11,7 @@
 
 (** The datatype of propositions; note mixfix syntax **)
 consts
-  prop     :: "i"
+  prop     :: i
 
 datatype
   "prop" = Fls
@@ -20,8 +20,8 @@
 
 (** 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)"
@@ -39,10 +39,10 @@
 
 (** 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
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Ramsey.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -20,9 +20,9 @@
 
 Ramsey = Arith +
 consts
-  Symmetric   		:: "i=>o"
-  Atleast     		:: "[i,i]=>o"
-  Clique,Indept,Ramsey	:: "[i,i,i]=>o"
+  Symmetric   		:: i=>o
+  Atleast     		:: [i,i]=>o
+  Clique,Indept,Ramsey	:: [i,i,i]=>o
 
 defs
 
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Rmap.thy
--- a/src/ZF/ex/Rmap.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Rmap.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,7 +9,7 @@
 Rmap = List +
 
 consts
-  rmap :: "i=>i"
+  rmap :: i=>i
 
 inductive
   domains "rmap(r)" <= "list(domain(r))*list(range(r))"
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/TF.thy
--- a/src/ZF/ex/TF.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/TF.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,14 +8,14 @@
 
 TF = List +
 consts
-  TF_rec      :: "[i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i"
-  TF_map      :: "[i=>i, i] => i"
-  TF_size     :: "i=>i"
-  TF_preorder :: "i=>i"
-  list_of_TF  :: "i=>i"
-  TF_of_list  :: "i=>i"
+  TF_rec      :: [i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i
+  TF_map      :: [i=>i, i] => i
+  TF_size     :: i=>i
+  TF_preorder :: i=>i
+  list_of_TF  :: i=>i
+  TF_of_list  :: i=>i
 
-  tree, forest, tree_forest    :: "i=>i"
+  tree, forest, tree_forest    :: i=>i
 
 datatype
   "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
diff -r 5d909faf0e04 -r 0c439768f45c src/ZF/ex/Term.thy
--- a/src/ZF/ex/Term.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/ex/Term.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -9,13 +9,13 @@
 
 Term = List +
 consts
-  term_rec  :: "[i, [i,i,i]=>i] => i"
-  term_map  :: "[i=>i, i] => i"
-  term_size :: "i=>i"
-  reflect   :: "i=>i"
-  preorder  :: "i=>i"
+  term_rec  :: [i, [i,i,i]=>i] => i
+  term_map  :: [i=>i, i] => i
+  term_size :: i=>i
+  reflect   :: i=>i
+  preorder  :: i=>i
 
-  term      :: "i=>i"
+  term      :: i=>i
 
 datatype
   "term(A)" = Apply ("a: A", "l: list(term(A))")