removed quotes from consts and syntax sections
authorclasohm
Sat Dec 09 13:36:11 1995 +0100 (1995-12-09)
changeset 14010c439768f45c
parent 1400 5d909faf0e04
child 1402 b72ccd1cff02
removed quotes from consts and syntax sections
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/AC18_AC19.thy
src/ZF/AC/AC_Equiv.thy
src/ZF/AC/DC.thy
src/ZF/AC/HH.thy
src/ZF/AC/Hartog.thy
src/ZF/AC/OrdQuant.thy
src/ZF/AC/Transrec2.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/AC/first.thy
src/ZF/AC/recfunAC16.thy
src/ZF/Arith.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Coind/BCR.thy
src/ZF/Coind/Dynamic.thy
src/ZF/Coind/ECR.thy
src/ZF/Coind/Language.thy
src/ZF/Coind/Map.thy
src/ZF/Coind/Static.thy
src/ZF/Coind/Types.thy
src/ZF/Coind/Values.thy
src/ZF/Epsilon.thy
src/ZF/EquivClass.thy
src/ZF/Finite.thy
src/ZF/Fixedpt.thy
src/ZF/IMP/Com.thy
src/ZF/IMP/Denotation.thy
src/ZF/Let.thy
src/ZF/List.thy
src/ZF/Nat.thy
src/ZF/Order.thy
src/ZF/OrderArith.thy
src/ZF/OrderType.thy
src/ZF/Ordinal.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Rel.thy
src/ZF/Resid/Confluence.thy
src/ZF/Resid/Conversion.thy
src/ZF/Resid/Redex.thy
src/ZF/Resid/Reduction.thy
src/ZF/Resid/Residuals.thy
src/ZF/Resid/SubUnion.thy
src/ZF/Resid/Substitution.thy
src/ZF/Resid/Terms.thy
src/ZF/Sum.thy
src/ZF/Trancl.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/ZF.thy
src/ZF/Zorn.thy
src/ZF/ex/Acc.thy
src/ZF/ex/BT.thy
src/ZF/ex/Bin.thy
src/ZF/ex/Brouwer.thy
src/ZF/ex/CoUnit.thy
src/ZF/ex/Comb.thy
src/ZF/ex/Data.thy
src/ZF/ex/Enum.thy
src/ZF/ex/Integ.thy
src/ZF/ex/LList.thy
src/ZF/ex/Limit.thy
src/ZF/ex/ListN.thy
src/ZF/ex/Ntree.thy
src/ZF/ex/Primrec.thy
src/ZF/ex/PropLog.thy
src/ZF/ex/Ramsey.thy
src/ZF/ex/Rmap.thy
src/ZF/ex/TF.thy
src/ZF/ex/Term.thy
     1.1 --- a/src/ZF/AC/AC16_WO4.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/AC/AC16_WO4.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -7,11 +7,11 @@
     1.4  
     1.5  consts
     1.6  
     1.7 -  ww  :: "[i, i] => i"
     1.8 -  s_u :: "[i, i, i, i] => i"
     1.9 -  MM  :: "[i, i, i] => i"
    1.10 -  LL  :: "[i, i, i] => i"
    1.11 -  GG  :: "[i, i, i] => i"
    1.12 +  ww  :: [i, i] => i
    1.13 +  s_u :: [i, i, i, i] => i
    1.14 +  MM  :: [i, i, i] => i
    1.15 +  LL  :: [i, i, i] => i
    1.16 +  GG  :: [i, i, i] => i
    1.17    
    1.18  defs
    1.19  
     2.1 --- a/src/ZF/AC/AC18_AC19.thy	Fri Dec 08 19:48:15 1995 +0100
     2.2 +++ b/src/ZF/AC/AC18_AC19.thy	Sat Dec 09 13:36:11 1995 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  AC18_AC19 = AC_Equiv +
     2.5  
     2.6  consts
     2.7 -  u_    :: "i => i"
     2.8 +  u_    :: i => i
     2.9    
    2.10  defs
    2.11  
     3.1 --- a/src/ZF/AC/AC_Equiv.thy	Fri Dec 08 19:48:15 1995 +0100
     3.2 +++ b/src/ZF/AC/AC_Equiv.thy	Sat Dec 09 13:36:11 1995 +0100
     3.3 @@ -17,19 +17,19 @@
     3.4  consts
     3.5    
     3.6  (* Well Ordering Theorems *)
     3.7 -  WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: "o"
     3.8 -  WO4                               :: "i => o"
     3.9 +  WO1, WO2, WO3, WO5, WO6, WO7, WO8 :: o
    3.10 +  WO4                               :: i => o
    3.11  
    3.12  (* Axioms of Choice *)  
    3.13    AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9,
    3.14 -  AC11, AC12, AC14, AC15, AC17, AC19 :: "o"
    3.15 -  AC10, AC13              :: "i => o"
    3.16 -  AC16                    :: "[i, i] => o"
    3.17 -  AC18                    :: "prop"       ("AC18")
    3.18 +  AC11, AC12, AC14, AC15, AC17, AC19 :: o
    3.19 +  AC10, AC13              :: i => o
    3.20 +  AC16                    :: [i, i] => o
    3.21 +  AC18                    :: prop       ("AC18")
    3.22  
    3.23  (* Auxiliary definitions used in definitions *)
    3.24 -  pairwise_disjoint       :: "i => o"
    3.25 -  sets_of_size_between    :: "[i, i, i] => o"
    3.26 +  pairwise_disjoint       :: i => o
    3.27 +  sets_of_size_between    :: [i, i, i] => o
    3.28  
    3.29  defs
    3.30  
     4.1 --- a/src/ZF/AC/DC.thy	Fri Dec 08 19:48:15 1995 +0100
     4.2 +++ b/src/ZF/AC/DC.thy	Sat Dec 09 13:36:11 1995 +0100
     4.3 @@ -9,9 +9,9 @@
     4.4  
     4.5  consts
     4.6  
     4.7 -  DC  :: "i => o"
     4.8 -  DC0 :: "o"
     4.9 -  ff  :: "[i, i, i, i] => i"
    4.10 +  DC  :: i => o
    4.11 +  DC0 :: o
    4.12 +  ff  :: [i, i, i, i] => i
    4.13  
    4.14  rules
    4.15  
     5.1 --- a/src/ZF/AC/HH.thy	Fri Dec 08 19:48:15 1995 +0100
     5.2 +++ b/src/ZF/AC/HH.thy	Sat Dec 09 13:36:11 1995 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4  
     5.5  consts
     5.6   
     5.7 -  HH                      :: "[i, i, i] => i"
     5.8 +  HH                      :: [i, i, i] => i
     5.9  
    5.10  defs
    5.11  
     6.1 --- a/src/ZF/AC/Hartog.thy	Fri Dec 08 19:48:15 1995 +0100
     6.2 +++ b/src/ZF/AC/Hartog.thy	Sat Dec 09 13:36:11 1995 +0100
     6.3 @@ -9,7 +9,7 @@
     6.4  
     6.5  consts
     6.6  
     6.7 -  Hartog :: "i => i"
     6.8 +  Hartog :: i => i
     6.9  
    6.10  defs
    6.11  
     7.1 --- a/src/ZF/AC/OrdQuant.thy	Fri Dec 08 19:48:15 1995 +0100
     7.2 +++ b/src/ZF/AC/OrdQuant.thy	Sat Dec 09 13:36:11 1995 +0100
     7.3 @@ -10,16 +10,16 @@
     7.4  consts
     7.5    
     7.6    (* Ordinal Quantifiers *)
     7.7 -  oall, oex   :: "[i, i => o] => o"
     7.8 +  oall, oex   :: [i, i => o] => o
     7.9  
    7.10    (* Ordinal Union *)
    7.11 -  OUnion      :: "[i, i => i] => i"
    7.12 +  OUnion      :: [i, i => i] => i
    7.13    
    7.14  syntax
    7.15    
    7.16 -  "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
    7.17 -  "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
    7.18 -  "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
    7.19 +  "@oall"     :: [idt, i, o] => o        ("(3ALL _<_./ _)" 10)
    7.20 +  "@oex"      :: [idt, i, o] => o        ("(3EX _<_./ _)" 10)
    7.21 +  "@OUNION"   :: [idt, i, i] => i        ("(3UN _<_./ _)" 10)
    7.22  
    7.23  translations
    7.24    
     8.1 --- a/src/ZF/AC/Transrec2.thy	Fri Dec 08 19:48:15 1995 +0100
     8.2 +++ b/src/ZF/AC/Transrec2.thy	Sat Dec 09 13:36:11 1995 +0100
     8.3 @@ -10,7 +10,7 @@
     8.4  
     8.5  consts
     8.6    
     8.7 -  transrec2               :: "[i, i, [i,i]=>i] =>i"
     8.8 +  transrec2               :: [i, i, [i,i]=>i] =>i
     8.9  
    8.10  defs
    8.11  
     9.1 --- a/src/ZF/AC/WO6_WO1.thy	Fri Dec 08 19:48:15 1995 +0100
     9.2 +++ b/src/ZF/AC/WO6_WO1.thy	Sat Dec 09 13:36:11 1995 +0100
     9.3 @@ -12,10 +12,10 @@
     9.4  
     9.5  consts
     9.6  (* Auxiliary definitions used in proof *)
     9.7 -  NN            :: "i => i"
     9.8 -  uu            :: "[i, i, i, i] => i"
     9.9 -  vv1, ww1, gg1 :: "[i, i, i] => i"
    9.10 -  vv2, ww2, gg2 :: "[i, i, i, i] => i"
    9.11 +  NN            :: i => i
    9.12 +  uu            :: [i, i, i, i] => i
    9.13 +  vv1, ww1, gg1 :: [i, i, i] => i
    9.14 +  vv2, ww2, gg2 :: [i, i, i, i] => i
    9.15  
    9.16  defs
    9.17  
    10.1 --- a/src/ZF/AC/first.thy	Fri Dec 08 19:48:15 1995 +0100
    10.2 +++ b/src/ZF/AC/first.thy	Sat Dec 09 13:36:11 1995 +0100
    10.3 @@ -9,7 +9,7 @@
    10.4  
    10.5  consts
    10.6  
    10.7 -  first                   :: "[i, i, i] => o"
    10.8 +  first                   :: [i, i, i] => o
    10.9  
   10.10  defs
   10.11  
    11.1 --- a/src/ZF/AC/recfunAC16.thy	Fri Dec 08 19:48:15 1995 +0100
    11.2 +++ b/src/ZF/AC/recfunAC16.thy	Sat Dec 09 13:36:11 1995 +0100
    11.3 @@ -9,7 +9,7 @@
    11.4  
    11.5  consts
    11.6  
    11.7 -  recfunAC16              :: "[i, i, i, i] => i"
    11.8 +  recfunAC16              :: [i, i, i, i] => i
    11.9  
   11.10  defs
   11.11  
    12.1 --- a/src/ZF/Arith.thy	Fri Dec 08 19:48:15 1995 +0100
    12.2 +++ b/src/ZF/Arith.thy	Sat Dec 09 13:36:11 1995 +0100
    12.3 @@ -8,12 +8,12 @@
    12.4  
    12.5  Arith = Epsilon + "simpdata" +
    12.6  consts
    12.7 -    rec  :: "[i, i, [i,i]=>i]=>i"
    12.8 -    "#*" :: "[i,i]=>i"      		(infixl 70)
    12.9 -    div  :: "[i,i]=>i"      		(infixl 70) 
   12.10 -    mod  :: "[i,i]=>i"      		(infixl 70)
   12.11 -    "#+" :: "[i,i]=>i"      		(infixl 65)
   12.12 -    "#-" :: "[i,i]=>i"      		(infixl 65)
   12.13 +    rec  :: [i, i, [i,i]=>i]=>i
   12.14 +    "#*" :: [i,i]=>i      		(infixl 70)
   12.15 +    div  :: [i,i]=>i      		(infixl 70) 
   12.16 +    mod  :: [i,i]=>i      		(infixl 70)
   12.17 +    "#+" :: [i,i]=>i      		(infixl 65)
   12.18 +    "#-" :: [i,i]=>i      		(infixl 65)
   12.19  
   12.20  defs
   12.21      rec_def  "rec(k,a,b) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
    13.1 --- a/src/ZF/Bool.thy	Fri Dec 08 19:48:15 1995 +0100
    13.2 +++ b/src/ZF/Bool.thy	Sat Dec 09 13:36:11 1995 +0100
    13.3 @@ -10,14 +10,14 @@
    13.4  
    13.5  Bool = ZF + "simpdata" +
    13.6  consts
    13.7 -    "1"		:: "i"     	   ("1")
    13.8 -    "2"         :: "i"             ("2")
    13.9 -    bool        :: "i"
   13.10 -    cond        :: "[i,i,i]=>i"
   13.11 -    not		:: "i=>i"
   13.12 -    "and"       :: "[i,i]=>i"      (infixl 70)
   13.13 -    or		:: "[i,i]=>i"      (infixl 65)
   13.14 -    xor		:: "[i,i]=>i"      (infixl 65)
   13.15 +    "1"		:: i     	   ("1")
   13.16 +    "2"         :: i             ("2")
   13.17 +    bool        :: i
   13.18 +    cond        :: [i,i,i]=>i
   13.19 +    not		:: i=>i
   13.20 +    "and"       :: [i,i]=>i      (infixl 70)
   13.21 +    or		:: [i,i]=>i      (infixl 65)
   13.22 +    xor		:: [i,i]=>i      (infixl 65)
   13.23  
   13.24  translations
   13.25     "1"  == "succ(0)"
    14.1 --- a/src/ZF/Cardinal.thy	Fri Dec 08 19:48:15 1995 +0100
    14.2 +++ b/src/ZF/Cardinal.thy	Sat Dec 09 13:36:11 1995 +0100
    14.3 @@ -8,11 +8,11 @@
    14.4  
    14.5  Cardinal = OrderType + Fixedpt + Nat + Sum + 
    14.6  consts
    14.7 -  Least            :: "(i=>o) => i"    (binder "LEAST " 10)
    14.8 +  Least            :: (i=>o) => i    (binder "LEAST " 10)
    14.9    eqpoll, lepoll,
   14.10 -          lesspoll :: "[i,i] => o"     (infixl 50)
   14.11 -  cardinal         :: "i=>i"           ("|_|")
   14.12 -  Finite, Card     :: "i=>o"
   14.13 +          lesspoll :: [i,i] => o     (infixl 50)
   14.14 +  cardinal         :: i=>i           ("|_|")
   14.15 +  Finite, Card     :: i=>o
   14.16  
   14.17  defs
   14.18  
    15.1 --- a/src/ZF/CardinalArith.thy	Fri Dec 08 19:48:15 1995 +0100
    15.2 +++ b/src/ZF/CardinalArith.thy	Sat Dec 09 13:36:11 1995 +0100
    15.3 @@ -9,12 +9,12 @@
    15.4  CardinalArith = Cardinal + OrderArith + Arith + Finite + 
    15.5  consts
    15.6  
    15.7 -  InfCard       :: "i=>o"
    15.8 -  "|*|"         :: "[i,i]=>i"       (infixl 70)
    15.9 -  "|+|"         :: "[i,i]=>i"       (infixl 65)
   15.10 -  csquare_rel   :: "i=>i"
   15.11 -  jump_cardinal :: "i=>i"
   15.12 -  csucc         :: "i=>i"
   15.13 +  InfCard       :: i=>o
   15.14 +  "|*|"         :: [i,i]=>i       (infixl 70)
   15.15 +  "|+|"         :: [i,i]=>i       (infixl 65)
   15.16 +  csquare_rel   :: i=>i
   15.17 +  jump_cardinal :: i=>i
   15.18 +  csucc         :: i=>i
   15.19  
   15.20  defs
   15.21  
    16.1 --- a/src/ZF/Coind/BCR.thy	Fri Dec 08 19:48:15 1995 +0100
    16.2 +++ b/src/ZF/Coind/BCR.thy	Sat Dec 09 13:36:11 1995 +0100
    16.3 @@ -10,14 +10,14 @@
    16.4    parameter of the proof.  A concrete version could be defined inductively.*)
    16.5  
    16.6  consts
    16.7 -  isof :: "[i,i] => o"
    16.8 +  isof :: [i,i] => o
    16.9  rules
   16.10    isof_app "[| isof(c1,t_fun(t1,t2)); isof(c2,t1) |] ==> isof(c_app(c1,c2),t2)"
   16.11  
   16.12  (*Its extension to environments*)
   16.13  
   16.14  consts
   16.15 -  isofenv :: "[i,i] => o"
   16.16 +  isofenv :: [i,i] => o
   16.17  defs
   16.18    isofenv_def "isofenv(ve,te) ==   		
   16.19     ve_dom(ve) = te_dom(te) &   		
    17.1 --- a/src/ZF/Coind/Dynamic.thy	Fri Dec 08 19:48:15 1995 +0100
    17.2 +++ b/src/ZF/Coind/Dynamic.thy	Sat Dec 09 13:36:11 1995 +0100
    17.3 @@ -7,7 +7,7 @@
    17.4  Dynamic = Values +
    17.5  
    17.6  consts
    17.7 -  EvalRel :: "i"
    17.8 +  EvalRel :: i
    17.9  inductive
   17.10    domains "EvalRel" <= "ValEnv * Exp * Val"
   17.11    intrs
    18.1 --- a/src/ZF/Coind/ECR.thy	Fri Dec 08 19:48:15 1995 +0100
    18.2 +++ b/src/ZF/Coind/ECR.thy	Sat Dec 09 13:36:11 1995 +0100
    18.3 @@ -9,7 +9,7 @@
    18.4  (* The extended correspondence relation *)
    18.5  
    18.6  consts
    18.7 -  HasTyRel :: "i"
    18.8 +  HasTyRel :: i
    18.9  coinductive
   18.10    domains "HasTyRel" <= "Val * Ty"
   18.11    intrs
   18.12 @@ -28,7 +28,7 @@
   18.13  (* Pointwise extension to environments *)
   18.14   
   18.15  consts
   18.16 -  hastyenv :: "[i,i] => o"
   18.17 +  hastyenv :: [i,i] => o
   18.18  defs
   18.19    hastyenv_def 
   18.20      " hastyenv(ve,te) == 			
    19.1 --- a/src/ZF/Coind/Language.thy	Fri Dec 08 19:48:15 1995 +0100
    19.2 +++ b/src/ZF/Coind/Language.thy	Sat Dec 09 13:36:11 1995 +0100
    19.3 @@ -7,8 +7,8 @@
    19.4  Language ="Datatype" + QUniv +
    19.5  
    19.6  consts
    19.7 -  Const :: "i"			(* Abstract type of constants *)
    19.8 -  c_app :: "[i,i] => i"		(*Abstract constructor for fun application*)
    19.9 +  Const :: i			(* Abstract type of constants *)
   19.10 +  c_app :: [i,i] => i		(*Abstract constructor for fun application*)
   19.11  
   19.12  rules
   19.13    constNEE  "c:Const ==> c ~= 0"
   19.14 @@ -16,8 +16,8 @@
   19.15  
   19.16  
   19.17  consts
   19.18 -  Exp   :: "i"			(* Datatype of expressions *)
   19.19 -  ExVar :: "i"			(* Abstract type of variables *)
   19.20 +  Exp   :: i			(* Datatype of expressions *)
   19.21 +  ExVar :: i			(* Abstract type of variables *)
   19.22  datatype <= "univ(Const Un ExVar)"
   19.23    "Exp" = e_const("c:Const")
   19.24          | e_var("x:ExVar")
    20.1 --- a/src/ZF/Coind/Map.thy	Fri Dec 08 19:48:15 1995 +0100
    20.2 +++ b/src/ZF/Coind/Map.thy	Sat Dec 09 13:36:11 1995 +0100
    20.3 @@ -7,8 +7,8 @@
    20.4  Map = QUniv +
    20.5  
    20.6  consts
    20.7 -  TMap :: "[i,i] => i"
    20.8 -  PMap :: "[i,i] => i"
    20.9 +  TMap :: [i,i] => i
   20.10 +  PMap :: [i,i] => i
   20.11  defs
   20.12    TMap_def "TMap(A,B) == {m:Pow(A*Union(B)).ALL a:A.m``{a}:B}"
   20.13    PMap_def "PMap(A,B) == TMap(A,cons(0,B))"
   20.14 @@ -16,9 +16,9 @@
   20.15  (* Note: 0:B ==> TMap(A,B) = PMap(A,B) *)
   20.16    
   20.17  consts
   20.18 -  map_emp :: "i"
   20.19 -  map_owr :: "[i,i,i]=>i"
   20.20 -  map_app :: "[i,i]=>i"
   20.21 +  map_emp :: i
   20.22 +  map_owr :: [i,i,i]=>i
   20.23 +  map_app :: [i,i]=>i
   20.24  defs
   20.25    map_emp_def "map_emp == 0"
   20.26    map_owr_def "map_owr(m,a,b) == SUM x:{a} Un domain(m).if(x=a,b,m``{x})"
    21.1 --- a/src/ZF/Coind/Static.thy	Fri Dec 08 19:48:15 1995 +0100
    21.2 +++ b/src/ZF/Coind/Static.thy	Sat Dec 09 13:36:11 1995 +0100
    21.3 @@ -7,7 +7,7 @@
    21.4  Static = BCR +
    21.5  
    21.6  consts
    21.7 -  ElabRel :: "i"
    21.8 +  ElabRel :: i
    21.9  inductive
   21.10    domains "ElabRel" <= "TyEnv * Exp * Ty"
   21.11    intrs
    22.1 --- a/src/ZF/Coind/Types.thy	Fri Dec 08 19:48:15 1995 +0100
    22.2 +++ b/src/ZF/Coind/Types.thy	Sat Dec 09 13:36:11 1995 +0100
    22.3 @@ -7,8 +7,8 @@
    22.4  Types = Language +
    22.5  
    22.6  consts
    22.7 -  Ty :: "i"			(* Datatype of types *)
    22.8 -  TyConst :: "i"		(* Abstract type of type constants *)
    22.9 +  Ty :: i			(* Datatype of types *)
   22.10 +  TyConst :: i		(* Abstract type of type constants *)
   22.11  datatype <= "univ(TyConst)"
   22.12    "Ty" = t_const("tc:TyConst")
   22.13         | t_fun("t1:Ty","t2:Ty")
   22.14 @@ -17,21 +17,21 @@
   22.15  (* Definition of type environments and associated operators *)
   22.16  
   22.17  consts
   22.18 -  TyEnv :: "i"
   22.19 +  TyEnv :: i
   22.20  datatype <= "univ(Ty Un ExVar)"
   22.21    "TyEnv" = te_emp
   22.22            | te_owr("te:TyEnv","x:ExVar","t:Ty") 
   22.23  
   22.24  consts
   22.25 -  te_rec :: "[i,i,[i,i,i,i]=>i] => i"
   22.26 +  te_rec :: [i,i,[i,i,i,i]=>i] => i
   22.27  defs
   22.28    te_rec_def
   22.29      "te_rec(te,c,h) ==   
   22.30      Vrec(te,%te g.TyEnv_case(c,%tem x t.h(tem,x,t,g`tem),te))"
   22.31    
   22.32  consts
   22.33 -  te_dom :: "i => i"
   22.34 -  te_app :: "[i,i] => i"
   22.35 +  te_dom :: i => i
   22.36 +  te_app :: [i,i] => i
   22.37  defs
   22.38    te_dom_def "te_dom(te) == te_rec(te,0,% te x t r.r Un {x})"
   22.39    te_app_def "te_app(te,x) == te_rec(te,0, % te y t r.if(x=y,t,r))"
    23.1 --- a/src/ZF/Coind/Values.thy	Fri Dec 08 19:48:15 1995 +0100
    23.2 +++ b/src/ZF/Coind/Values.thy	Sat Dec 09 13:36:11 1995 +0100
    23.3 @@ -9,7 +9,7 @@
    23.4  (* Values, values environments and associated operators *)
    23.5  
    23.6  consts
    23.7 -  Val, ValEnv, Val_ValEnv  :: "i"
    23.8 +  Val, ValEnv, Val_ValEnv  :: i
    23.9  codatatype <= "quniv(Const Un ExVar Un Exp)"
   23.10      "Val" = v_const("c:Const")
   23.11            | v_clos("x:ExVar","e:Exp","ve:ValEnv")
   23.12 @@ -19,10 +19,10 @@
   23.13    type_intrs "[A_into_univ, mapQU]"
   23.14  
   23.15  consts
   23.16 -  ve_emp :: "i"
   23.17 -  ve_owr :: "[i,i,i] => i"
   23.18 -  ve_dom :: "i=>i"
   23.19 -  ve_app :: "[i,i] => i"
   23.20 +  ve_emp :: i
   23.21 +  ve_owr :: [i,i,i] => i
   23.22 +  ve_dom :: i=>i
   23.23 +  ve_app :: [i,i] => i
   23.24  defs
   23.25    ve_emp_def "ve_emp == ve_mk(map_emp)"
   23.26    ve_owr_def
    24.1 --- a/src/ZF/Epsilon.thy	Fri Dec 08 19:48:15 1995 +0100
    24.2 +++ b/src/ZF/Epsilon.thy	Sat Dec 09 13:36:11 1995 +0100
    24.3 @@ -8,8 +8,8 @@
    24.4  
    24.5  Epsilon = Nat + "mono" +
    24.6  consts
    24.7 -    eclose,rank ::      "i=>i"
    24.8 -    transrec    ::      "[i, [i,i]=>i] =>i"
    24.9 +    eclose,rank ::      i=>i
   24.10 +    transrec    ::      [i, [i,i]=>i] =>i
   24.11  
   24.12  defs
   24.13    eclose_def	"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
    25.1 --- a/src/ZF/EquivClass.thy	Fri Dec 08 19:48:15 1995 +0100
    25.2 +++ b/src/ZF/EquivClass.thy	Sat Dec 09 13:36:11 1995 +0100
    25.3 @@ -8,9 +8,9 @@
    25.4  
    25.5  EquivClass = Rel + Perm + 
    25.6  consts
    25.7 -    "'/"        ::      "[i,i]=>i"  (infixl 90)  (*set of equiv classes*)
    25.8 -    congruent	::	"[i,i=>i]=>o"
    25.9 -    congruent2  ::      "[i,[i,i]=>i]=>o"
   25.10 +    "'/"        ::      [i,i]=>i  (infixl 90)  (*set of equiv classes*)
   25.11 +    congruent	::	[i,i=>i]=>o
   25.12 +    congruent2  ::      [i,[i,i]=>i]=>o
   25.13  
   25.14  defs
   25.15      quotient_def  "A/r == {r``{x} . x:A}"
    26.1 --- a/src/ZF/Finite.thy	Fri Dec 08 19:48:15 1995 +0100
    26.2 +++ b/src/ZF/Finite.thy	Sat Dec 09 13:36:11 1995 +0100
    26.3 @@ -8,8 +8,8 @@
    26.4  
    26.5  Finite = Arith + Inductive +
    26.6  consts
    26.7 -  Fin 	    :: "i=>i"
    26.8 -  FiniteFun :: "[i,i]=>i"		("(_ -||>/ _)" [61, 60] 60)
    26.9 +  Fin 	    :: i=>i
   26.10 +  FiniteFun :: [i,i]=>i		("(_ -||>/ _)" [61, 60] 60)
   26.11  
   26.12  inductive
   26.13    domains   "Fin(A)" <= "Pow(A)"
    27.1 --- a/src/ZF/Fixedpt.thy	Fri Dec 08 19:48:15 1995 +0100
    27.2 +++ b/src/ZF/Fixedpt.thy	Sat Dec 09 13:36:11 1995 +0100
    27.3 @@ -8,8 +8,8 @@
    27.4  
    27.5  Fixedpt = ZF + "domrange" +
    27.6  consts
    27.7 -  bnd_mono    :: "[i,i=>i]=>o"
    27.8 -  lfp, gfp    :: "[i,i=>i]=>i"
    27.9 +  bnd_mono    :: [i,i=>i]=>o
   27.10 +  lfp, gfp    :: [i,i=>i]=>i
   27.11  
   27.12  defs
   27.13    (*monotone operator from Pow(D) to itself*)
    28.1 --- a/src/ZF/IMP/Com.thy	Fri Dec 08 19:48:15 1995 +0100
    28.2 +++ b/src/ZF/IMP/Com.thy	Sat Dec 09 13:36:11 1995 +0100
    28.3 @@ -11,8 +11,8 @@
    28.4  Com = Datatype +
    28.5  
    28.6  (** Arithmetic expressions **)
    28.7 -consts  loc  :: "i"
    28.8 -        aexp :: "i"
    28.9 +consts  loc  :: i
   28.10 +        aexp :: i
   28.11  
   28.12  datatype <= "univ(loc Un (nat->nat) Un ((nat*nat) -> nat) )"
   28.13    "aexp" = N ("n: nat")
   28.14 @@ -22,8 +22,8 @@
   28.15  
   28.16  
   28.17  (** Evaluation of arithmetic expressions **)
   28.18 -consts  evala    :: "i"
   28.19 -       "@evala"  :: "[i,i,i] => o"		("<_,_>/ -a-> _"  [0,0,50] 50)
   28.20 +consts  evala    :: i
   28.21 +       "@evala"  :: [i,i,i] => o		("<_,_>/ -a-> _"  [0,0,50] 50)
   28.22  translations
   28.23      "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
   28.24  inductive
   28.25 @@ -39,7 +39,7 @@
   28.26  
   28.27  
   28.28  (** Boolean expressions **)
   28.29 -consts  bexp :: "i"
   28.30 +consts  bexp :: i
   28.31  
   28.32  datatype <= "univ(aexp Un ((nat*nat)->bool) )"
   28.33    "bexp" = true
   28.34 @@ -51,8 +51,8 @@
   28.35  
   28.36  
   28.37  (** Evaluation of boolean expressions **)
   28.38 -consts evalb	:: "i"	
   28.39 -       "@evalb" :: "[i,i,i] => o"		("<_,_>/ -b-> _" [0,0,50] 50)
   28.40 +consts evalb	:: i	
   28.41 +       "@evalb" :: [i,i,i] => o		("<_,_>/ -b-> _" [0,0,50] 50)
   28.42  
   28.43  translations
   28.44      "<be,sig> -b-> b" == "<be,sig,b> : evalb"
   28.45 @@ -76,7 +76,7 @@
   28.46  
   28.47  
   28.48  (** Commands **)
   28.49 -consts  com :: "i"
   28.50 +consts  com :: i
   28.51  
   28.52  datatype <= "univ(loc Un aexp Un bexp)"
   28.53    "com" = skip
   28.54 @@ -89,9 +89,9 @@
   28.55    with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)
   28.56  
   28.57  (** Execution of commands **)
   28.58 -consts  evalc    :: "i"
   28.59 -        "@evalc" :: "[i,i,i] => o"   		("<_,_>/ -c-> _" [0,0,50] 50)
   28.60 -	"assign" :: "[i,i,i] => i"   		("_[_'/_]"       [95,0,0] 95)
   28.61 +consts  evalc    :: i
   28.62 +        "@evalc" :: [i,i,i] => o   		("<_,_>/ -c-> _" [0,0,50] 50)
   28.63 +	"assign" :: [i,i,i] => i   		("_[_'/_]"       [95,0,0] 95)
   28.64  
   28.65  translations
   28.66         "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"
    29.1 --- a/src/ZF/IMP/Denotation.thy	Fri Dec 08 19:48:15 1995 +0100
    29.2 +++ b/src/ZF/IMP/Denotation.thy	Sat Dec 09 13:36:11 1995 +0100
    29.3 @@ -9,10 +9,10 @@
    29.4  Denotation = Com + 
    29.5  
    29.6  consts
    29.7 -  A     :: "i => i => i"
    29.8 -  B     :: "i => i => i"
    29.9 -  C     :: "i => i"
   29.10 -  Gamma :: "[i,i,i] => i"
   29.11 +  A     :: i => i => i
   29.12 +  B     :: i => i => i
   29.13 +  C     :: i => i
   29.14 +  Gamma :: [i,i,i] => i
   29.15  
   29.16  rules	(*NOT definitional*)
   29.17    A_nat_def	"A(N(n)) == (%sigma. n)"
    30.1 --- a/src/ZF/Let.thy	Fri Dec 08 19:48:15 1995 +0100
    30.2 +++ b/src/ZF/Let.thy	Sat Dec 09 13:36:11 1995 +0100
    30.3 @@ -12,13 +12,13 @@
    30.4    letbinds  letbind
    30.5  
    30.6  consts
    30.7 -  Let           :: "['a, 'a => 'b] => 'b"
    30.8 +  Let           :: ['a, 'a => 'b] => 'b
    30.9  
   30.10  syntax
   30.11 -  "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   30.12 -  ""            :: "letbind => letbinds"              ("_")
   30.13 -  "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   30.14 -  "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
   30.15 +  "_bind"       :: [pttrn, 'a] => letbind           ("(2_ =/ _)" 10)
   30.16 +  ""            :: letbind => letbinds              ("_")
   30.17 +  "_binds"      :: [letbind, letbinds] => letbinds  ("_;/ _")
   30.18 +  "_Let"        :: [letbinds, 'a] => 'a             ("(let (_)/ in (_))" 10)
   30.19  
   30.20  translations
   30.21    "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
    31.1 --- a/src/ZF/List.thy	Fri Dec 08 19:48:15 1995 +0100
    31.2 +++ b/src/ZF/List.thy	Sat Dec 09 13:36:11 1995 +0100
    31.3 @@ -13,20 +13,20 @@
    31.4  List = Datatype + 
    31.5  
    31.6  consts
    31.7 -  "@"	     :: "[i,i]=>i"      			(infixr 60)
    31.8 -  list_rec   :: "[i, i, [i,i,i]=>i] => i"
    31.9 -  map 	     :: "[i=>i, i] => i"
   31.10 -  length,rev :: "i=>i"
   31.11 -  flat       :: "i=>i"
   31.12 -  list_add   :: "i=>i"
   31.13 -  hd,tl      :: "i=>i"
   31.14 -  drop	     :: "[i,i]=>i"
   31.15 +  "@"	     :: [i,i]=>i      			(infixr 60)
   31.16 +  list_rec   :: [i, i, [i,i,i]=>i] => i
   31.17 +  map 	     :: [i=>i, i] => i
   31.18 +  length,rev :: i=>i
   31.19 +  flat       :: i=>i
   31.20 +  list_add   :: i=>i
   31.21 +  hd,tl      :: i=>i
   31.22 +  drop	     :: [i,i]=>i
   31.23  
   31.24   (* List Enumeration *)
   31.25 - "[]"        :: "i" 	                           	("[]")
   31.26 - "@List"     :: "is => i" 	                   	("[(_)]")
   31.27 + "[]"        :: i 	                           	("[]")
   31.28 + "@List"     :: is => i 	                   	("[(_)]")
   31.29  
   31.30 -  list	     :: "i=>i"
   31.31 +  list	     :: i=>i
   31.32  
   31.33    
   31.34  datatype
    32.1 --- a/src/ZF/Nat.thy	Fri Dec 08 19:48:15 1995 +0100
    32.2 +++ b/src/ZF/Nat.thy	Sat Dec 09 13:36:11 1995 +0100
    32.3 @@ -8,9 +8,9 @@
    32.4  
    32.5  Nat = Ordinal + Bool + "mono" +
    32.6  consts
    32.7 -    nat 	::      "i"
    32.8 -    nat_case    ::      "[i, i=>i, i]=>i"
    32.9 -    nat_rec     ::      "[i, i, [i,i]=>i]=>i"
   32.10 +    nat 	::      i
   32.11 +    nat_case    ::      [i, i=>i, i]=>i
   32.12 +    nat_rec     ::      [i, i, [i,i]=>i]=>i
   32.13  
   32.14  defs
   32.15  
    33.1 --- a/src/ZF/Order.thy	Fri Dec 08 19:48:15 1995 +0100
    33.2 +++ b/src/ZF/Order.thy	Sat Dec 09 13:36:11 1995 +0100
    33.3 @@ -8,13 +8,13 @@
    33.4  
    33.5  Order = WF + Perm + 
    33.6  consts
    33.7 -  part_ord        :: "[i,i]=>o"		(*Strict partial ordering*)
    33.8 -  linear, tot_ord :: "[i,i]=>o"		(*Strict total ordering*)
    33.9 -  well_ord        :: "[i,i]=>o"		(*Well-ordering*)
   33.10 -  mono_map        :: "[i,i,i,i]=>i"	(*Order-preserving maps*)
   33.11 -  ord_iso         :: "[i,i,i,i]=>i"	(*Order isomorphisms*)
   33.12 -  pred            :: "[i,i,i]=>i"	(*Set of predecessors*)
   33.13 -  ord_iso_map     :: "[i,i,i,i]=>i"	(*Construction for linearity theorem*)
   33.14 +  part_ord        :: [i,i]=>o		(*Strict partial ordering*)
   33.15 +  linear, tot_ord :: [i,i]=>o		(*Strict total ordering*)
   33.16 +  well_ord        :: [i,i]=>o		(*Well-ordering*)
   33.17 +  mono_map        :: [i,i,i,i]=>i	(*Order-preserving maps*)
   33.18 +  ord_iso         :: [i,i,i,i]=>i	(*Order isomorphisms*)
   33.19 +  pred            :: [i,i,i]=>i	(*Set of predecessors*)
   33.20 +  ord_iso_map     :: [i,i,i,i]=>i	(*Construction for linearity theorem*)
   33.21  
   33.22  defs
   33.23    part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
    34.1 --- a/src/ZF/OrderArith.thy	Fri Dec 08 19:48:15 1995 +0100
    34.2 +++ b/src/ZF/OrderArith.thy	Sat Dec 09 13:36:11 1995 +0100
    34.3 @@ -8,8 +8,8 @@
    34.4  
    34.5  OrderArith = Order + Sum + 
    34.6  consts
    34.7 -  radd, rmult      :: "[i,i,i,i]=>i"
    34.8 -  rvimage          :: "[i,i,i]=>i"
    34.9 +  radd, rmult      :: [i,i,i,i]=>i
   34.10 +  rvimage          :: [i,i,i]=>i
   34.11  
   34.12  defs
   34.13    (*disjoint sum of two relations; underlies ordinal addition*)
    35.1 --- a/src/ZF/OrderType.thy	Fri Dec 08 19:48:15 1995 +0100
    35.2 +++ b/src/ZF/OrderType.thy	Sat Dec 09 13:36:11 1995 +0100
    35.3 @@ -10,14 +10,14 @@
    35.4  
    35.5  OrderType = OrderArith + Ordinal + 
    35.6  consts
    35.7 -  ordermap  :: "[i,i]=>i"
    35.8 -  ordertype :: "[i,i]=>i"
    35.9 +  ordermap  :: [i,i]=>i
   35.10 +  ordertype :: [i,i]=>i
   35.11  
   35.12 -  Ord_alt   :: "i => o"   
   35.13 +  Ord_alt   :: i => o   
   35.14  
   35.15 -  "**"      :: "[i,i]=>i"           (infixl 70)
   35.16 -  "++"      :: "[i,i]=>i"           (infixl 65)
   35.17 -  "--"      :: "[i,i]=>i"           (infixl 65)
   35.18 +  "**"      :: [i,i]=>i           (infixl 70)
   35.19 +  "++"      :: [i,i]=>i           (infixl 65)
   35.20 +  "--"      :: [i,i]=>i           (infixl 65)
   35.21   
   35.22  
   35.23  defs
    36.1 --- a/src/ZF/Ordinal.thy	Fri Dec 08 19:48:15 1995 +0100
    36.2 +++ b/src/ZF/Ordinal.thy	Sat Dec 09 13:36:11 1995 +0100
    36.3 @@ -8,11 +8,11 @@
    36.4  
    36.5  Ordinal = WF + Bool + "simpdata" + "equalities" +
    36.6  consts
    36.7 -  Memrel      	:: "i=>i"
    36.8 -  Transset,Ord  :: "i=>o"
    36.9 -  "<"           :: "[i,i] => o"  (infixl 50) (*less than on ordinals*)
   36.10 -  "le"          :: "[i,i] => o"  (infixl 50) (*less than or equals*)
   36.11 -  Limit         :: "i=>o"
   36.12 +  Memrel      	:: i=>i
   36.13 +  Transset,Ord  :: i=>o
   36.14 +  "<"           :: [i,i] => o  (infixl 50) (*less than on ordinals*)
   36.15 +  "le"          :: [i,i] => o  (infixl 50) (*less than or equals*)
   36.16 +  Limit         :: i=>o
   36.17  
   36.18  translations
   36.19    "x le y"      == "x < succ(y)"
    37.1 --- a/src/ZF/Perm.thy	Fri Dec 08 19:48:15 1995 +0100
    37.2 +++ b/src/ZF/Perm.thy	Sat Dec 09 13:36:11 1995 +0100
    37.3 @@ -11,9 +11,9 @@
    37.4  
    37.5  Perm = ZF + "mono" +
    37.6  consts
    37.7 -    O    	::      "[i,i]=>i"      (infixr 60)
    37.8 -    id  	::      "i=>i"
    37.9 -    inj,surj,bij::      "[i,i]=>i"
   37.10 +    O    	::      [i,i]=>i      (infixr 60)
   37.11 +    id  	::      i=>i
   37.12 +    inj,surj,bij::      [i,i]=>i
   37.13  
   37.14  defs
   37.15  
    38.1 --- a/src/ZF/QPair.thy	Fri Dec 08 19:48:15 1995 +0100
    38.2 +++ b/src/ZF/QPair.thy	Sat Dec 09 13:36:11 1995 +0100
    38.3 @@ -13,19 +13,19 @@
    38.4  
    38.5  QPair = Sum + "simpdata" +
    38.6  consts
    38.7 -  QPair     :: "[i, i] => i"               	("<(_;/ _)>")
    38.8 -  qfst,qsnd :: "i => i"
    38.9 -  qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
   38.10 -  qconverse :: "i => i"
   38.11 -  QSigma    :: "[i, i => i] => i"
   38.12 +  QPair     :: [i, i] => i               	("<(_;/ _)>")
   38.13 +  qfst,qsnd :: i => i
   38.14 +  qsplit    :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
   38.15 +  qconverse :: i => i
   38.16 +  QSigma    :: [i, i => i] => i
   38.17  
   38.18 -  "<+>"     :: "[i,i]=>i"      			(infixr 65)
   38.19 -  QInl,QInr :: "i=>i"
   38.20 -  qcase     :: "[i=>i, i=>i, i]=>i"
   38.21 +  "<+>"     :: [i,i]=>i      			(infixr 65)
   38.22 +  QInl,QInr :: i=>i
   38.23 +  qcase     :: [i=>i, i=>i, i]=>i
   38.24  
   38.25  syntax
   38.26 -  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
   38.27 -  "<*>"     :: "[i, i] => i"         		(infixr 80)
   38.28 +  "@QSUM"   :: [idt, i, i] => i               ("(3QSUM _:_./ _)" 10)
   38.29 +  "<*>"     :: [i, i] => i         		(infixr 80)
   38.30  
   38.31  translations
   38.32    "QSUM x:A. B"  => "QSigma(A, %x. B)"
    39.1 --- a/src/ZF/QUniv.thy	Fri Dec 08 19:48:15 1995 +0100
    39.2 +++ b/src/ZF/QUniv.thy	Sat Dec 09 13:36:11 1995 +0100
    39.3 @@ -8,7 +8,7 @@
    39.4  
    39.5  QUniv = Univ + QPair + "mono" + "equalities" +
    39.6  consts
    39.7 -    quniv        :: "i=>i"
    39.8 +    quniv        :: i=>i
    39.9  
   39.10  defs
   39.11      quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
    40.1 --- a/src/ZF/Rel.thy	Fri Dec 08 19:48:15 1995 +0100
    40.2 +++ b/src/ZF/Rel.thy	Sat Dec 09 13:36:11 1995 +0100
    40.3 @@ -8,9 +8,9 @@
    40.4  
    40.5  Rel = ZF +
    40.6  consts
    40.7 -    refl,irrefl,equiv      :: "[i,i]=>o"
    40.8 -    sym,asym,antisym,trans :: "i=>o"
    40.9 -    trans_on               :: "[i,i]=>o"	("trans[_]'(_')")
   40.10 +    refl,irrefl,equiv      :: [i,i]=>o
   40.11 +    sym,asym,antisym,trans :: i=>o
   40.12 +    trans_on               :: [i,i]=>o	("trans[_]'(_')")
   40.13  
   40.14  defs
   40.15    refl_def     "refl(A,r) == (ALL x: A. <x,x> : r)"
    41.1 --- a/src/ZF/Resid/Confluence.thy	Fri Dec 08 19:48:15 1995 +0100
    41.2 +++ b/src/ZF/Resid/Confluence.thy	Sat Dec 09 13:36:11 1995 +0100
    41.3 @@ -8,8 +8,8 @@
    41.4  Confluence = Reduction+
    41.5  
    41.6  consts
    41.7 -  confluence	:: "i=>o"
    41.8 -  strip		:: "o"
    41.9 +  confluence	:: i=>o
   41.10 +  strip		:: o
   41.11  
   41.12  defs
   41.13    confluence_def "confluence(R) ==   
    42.1 --- a/src/ZF/Resid/Conversion.thy	Fri Dec 08 19:48:15 1995 +0100
    42.2 +++ b/src/ZF/Resid/Conversion.thy	Sat Dec 09 13:36:11 1995 +0100
    42.3 @@ -9,10 +9,10 @@
    42.4  Conversion = Confluence+
    42.5  
    42.6  consts
    42.7 -  Sconv1	:: "i"
    42.8 -  "<-1->"	:: "[i,i]=>o" (infixl 50)
    42.9 -  Sconv		:: "i"
   42.10 -  "<--->"	:: "[i,i]=>o" (infixl 50)
   42.11 +  Sconv1	:: i
   42.12 +  "<-1->"	:: [i,i]=>o (infixl 50)
   42.13 +  Sconv		:: i
   42.14 +  "<--->"	:: [i,i]=>o (infixl 50)
   42.15  
   42.16  translations
   42.17    "a<-1->b"    == "<a,b>:Sconv1"
    43.1 --- a/src/ZF/Resid/Redex.thy	Fri Dec 08 19:48:15 1995 +0100
    43.2 +++ b/src/ZF/Resid/Redex.thy	Sat Dec 09 13:36:11 1995 +0100
    43.3 @@ -7,7 +7,7 @@
    43.4  
    43.5  Redex = Univ +
    43.6  consts
    43.7 -  redexes     :: "i"
    43.8 +  redexes     :: i
    43.9  
   43.10  datatype
   43.11    "redexes" = Var ("n: nat")	        
   43.12 @@ -17,7 +17,7 @@
   43.13    
   43.14  
   43.15  consts
   43.16 -  redex_rec   	:: "[i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i"
   43.17 +  redex_rec   	:: [i, i=>i, [i,i]=>i, [i,i,i,i,i]=>i]=>i
   43.18   
   43.19  defs
   43.20    redex_rec_def
    44.1 --- a/src/ZF/Resid/Reduction.thy	Fri Dec 08 19:48:15 1995 +0100
    44.2 +++ b/src/ZF/Resid/Reduction.thy	Sat Dec 09 13:36:11 1995 +0100
    44.3 @@ -8,8 +8,8 @@
    44.4  Reduction = Terms+
    44.5  
    44.6  consts
    44.7 -  Sred1, Sred,  Spar_red1,Spar_red    :: "i"
    44.8 -  "-1->","--->","=1=>",   "===>"      :: "[i,i]=>o" (infixl 50)
    44.9 +  Sred1, Sred,  Spar_red1,Spar_red    :: i
   44.10 +  "-1->","--->","=1=>",   "===>"      :: [i,i]=>o (infixl 50)
   44.11  
   44.12  translations
   44.13    "a -1-> b" == "<a,b>:Sred1"
    45.1 --- a/src/ZF/Resid/Residuals.thy	Fri Dec 08 19:48:15 1995 +0100
    45.2 +++ b/src/ZF/Resid/Residuals.thy	Sat Dec 09 13:36:11 1995 +0100
    45.3 @@ -9,9 +9,9 @@
    45.4  Residuals = Substitution+
    45.5  
    45.6  consts
    45.7 -  Sres		:: "i"
    45.8 -  residuals	:: "[i,i,i]=>i"
    45.9 -  "|>"		:: "[i,i]=>i"     (infixl 70)
   45.10 +  Sres		:: i
   45.11 +  residuals	:: [i,i,i]=>i
   45.12 +  "|>"		:: [i,i]=>i     (infixl 70)
   45.13    
   45.14  translations
   45.15    "residuals(u,v,w)"  == "<u,v,w>:Sres"
    46.1 --- a/src/ZF/Resid/SubUnion.thy	Fri Dec 08 19:48:15 1995 +0100
    46.2 +++ b/src/ZF/Resid/SubUnion.thy	Sat Dec 09 13:36:11 1995 +0100
    46.3 @@ -8,10 +8,10 @@
    46.4  SubUnion = Redex +
    46.5  
    46.6  consts
    46.7 -  Ssub,Scomp,Sreg  :: "i"
    46.8 -  "<==","~"        :: "[i,i]=>o" (infixl 70)
    46.9 -  un               :: "[i,i]=>i" (infixl 70)
   46.10 -  regular	   :: "i=>o"
   46.11 +  Ssub,Scomp,Sreg  :: i
   46.12 +  "<==","~"        :: [i,i]=>o (infixl 70)
   46.13 +  un               :: [i,i]=>i (infixl 70)
   46.14 +  regular	   :: i=>o
   46.15    
   46.16  translations
   46.17    "a<==b"        == "<a,b>:Ssub"
    47.1 --- a/src/ZF/Resid/Substitution.thy	Fri Dec 08 19:48:15 1995 +0100
    47.2 +++ b/src/ZF/Resid/Substitution.thy	Sat Dec 09 13:36:11 1995 +0100
    47.3 @@ -8,10 +8,10 @@
    47.4  Substitution = SubUnion +
    47.5  
    47.6  consts
    47.7 -  lift_rec	:: "[i,i]=> i"
    47.8 -  lift		:: "i=>i"
    47.9 -  subst_rec	:: "[i,i,i]=> i"
   47.10 -  "'/"          :: "[i,i]=>i"  (infixl 70)  (*subst*)
   47.11 +  lift_rec	:: [i,i]=> i
   47.12 +  lift		:: i=>i
   47.13 +  subst_rec	:: [i,i,i]=> i
   47.14 +  "'/"          :: [i,i]=>i  (infixl 70)  (*subst*)
   47.15  translations
   47.16    "lift(r)"  == "lift_rec(r,0)"
   47.17    "u/v" == "subst_rec(u,v,0)"
    48.1 --- a/src/ZF/Resid/Terms.thy	Fri Dec 08 19:48:15 1995 +0100
    48.2 +++ b/src/ZF/Resid/Terms.thy	Sat Dec 09 13:36:11 1995 +0100
    48.3 @@ -8,9 +8,9 @@
    48.4  Terms = Cube+
    48.5  
    48.6  consts
    48.7 -  lambda	:: "i"
    48.8 -  unmark	:: "i=>i"
    48.9 -  Apl		:: "[i,i]=>i"
   48.10 +  lambda	:: i
   48.11 +  unmark	:: i=>i
   48.12 +  Apl		:: [i,i]=>i
   48.13  
   48.14  translations
   48.15    "Apl(n,m)" == "App(0,n,m)"
    49.1 --- a/src/ZF/Sum.thy	Fri Dec 08 19:48:15 1995 +0100
    49.2 +++ b/src/ZF/Sum.thy	Sat Dec 09 13:36:11 1995 +0100
    49.3 @@ -9,10 +9,10 @@
    49.4  
    49.5  Sum = Bool + "simpdata" +
    49.6  consts
    49.7 -    "+"    	:: "[i,i]=>i"      		(infixr 65)
    49.8 -    Inl,Inr     :: "i=>i"
    49.9 -    case        :: "[i=>i, i=>i, i]=>i"
   49.10 -    Part        :: "[i,i=>i] => i"
   49.11 +    "+"    	:: [i,i]=>i      		(infixr 65)
   49.12 +    Inl,Inr     :: i=>i
   49.13 +    case        :: [i=>i, i=>i, i]=>i
   49.14 +    Part        :: [i,i=>i] => i
   49.15  
   49.16  defs
   49.17      sum_def     "A+B == {0}*A Un {1}*B"
    50.1 --- a/src/ZF/Trancl.thy	Fri Dec 08 19:48:15 1995 +0100
    50.2 +++ b/src/ZF/Trancl.thy	Sat Dec 09 13:36:11 1995 +0100
    50.3 @@ -8,8 +8,8 @@
    50.4  
    50.5  Trancl = Fixedpt + Perm + "mono" + Rel + 
    50.6  consts
    50.7 -    rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
    50.8 -    trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
    50.9 +    rtrancl :: i=>i  ("(_^*)" [100] 100)  (*refl/transitive closure*)
   50.10 +    trancl  :: i=>i  ("(_^+)" [100] 100)  (*transitive closure*)
   50.11  
   50.12  defs
   50.13      rtrancl_def	"r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
    51.1 --- a/src/ZF/Univ.thy	Fri Dec 08 19:48:15 1995 +0100
    51.2 +++ b/src/ZF/Univ.thy	Sat Dec 09 13:36:11 1995 +0100
    51.3 @@ -13,10 +13,10 @@
    51.4  
    51.5  Univ = Arith + Sum + Finite + "mono" +
    51.6  consts
    51.7 -    Vfrom       :: "[i,i]=>i"
    51.8 -    Vset        :: "i=>i"
    51.9 -    Vrec        :: "[i, [i,i]=>i] =>i"
   51.10 -    univ        :: "i=>i"
   51.11 +    Vfrom       :: [i,i]=>i
   51.12 +    Vset        :: i=>i
   51.13 +    Vrec        :: [i, [i,i]=>i] =>i
   51.14 +    univ        :: i=>i
   51.15  
   51.16  translations
   51.17      "Vset(x)"   == 	"Vfrom(0,x)"
    52.1 --- a/src/ZF/WF.thy	Fri Dec 08 19:48:15 1995 +0100
    52.2 +++ b/src/ZF/WF.thy	Sat Dec 09 13:36:11 1995 +0100
    52.3 @@ -8,13 +8,13 @@
    52.4  
    52.5  WF = Trancl + "mono" + "equalities" +
    52.6  consts
    52.7 -  wf           :: "i=>o"
    52.8 -  wf_on        :: "[i,i]=>o"			("wf[_]'(_')")
    52.9 +  wf           :: i=>o
   52.10 +  wf_on        :: [i,i]=>o			("wf[_]'(_')")
   52.11  
   52.12 -  wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"
   52.13 -  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"	("wfrec[_]'(_,_,_')")
   52.14 -  is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
   52.15 -  the_recfun   :: "[i, i, [i,i]=>i] =>i"
   52.16 +  wftrec,wfrec :: [i, i, [i,i]=>i] =>i
   52.17 +  wfrec_on     :: [i, i, i, [i,i]=>i] =>i	("wfrec[_]'(_,_,_')")
   52.18 +  is_recfun    :: [i, i, [i,i]=>i, i] =>o
   52.19 +  the_recfun   :: [i, i, [i,i]=>i] =>i
   52.20  
   52.21  defs
   52.22    (*r is a well-founded relation*)
    53.1 --- a/src/ZF/ZF.thy	Fri Dec 08 19:48:15 1995 +0100
    53.2 +++ b/src/ZF/ZF.thy	Sat Dec 09 13:36:11 1995 +0100
    53.3 @@ -16,68 +16,68 @@
    53.4  
    53.5  consts
    53.6  
    53.7 -  "0"         :: "i"                  ("0")   (*the empty set*)
    53.8 -  Pow         :: "i => i"                     (*power sets*)
    53.9 -  Inf         :: "i"                          (*infinite set*)
   53.10 +  "0"         :: i                  ("0")   (*the empty set*)
   53.11 +  Pow         :: i => i                     (*power sets*)
   53.12 +  Inf         :: i                          (*infinite set*)
   53.13  
   53.14    (* Bounded Quantifiers *)
   53.15  
   53.16 -  Ball, Bex   :: "[i, i => o] => o"
   53.17 +  Ball, Bex   :: [i, i => o] => o
   53.18  
   53.19    (* General Union and Intersection *)
   53.20  
   53.21 -  Union,Inter :: "i => i"
   53.22 +  Union,Inter :: i => i
   53.23  
   53.24    (* Variations on Replacement *)
   53.25  
   53.26 -  PrimReplace :: "[i, [i, i] => o] => i"
   53.27 -  Replace     :: "[i, [i, i] => o] => i"
   53.28 -  RepFun      :: "[i, i => i] => i"
   53.29 -  Collect     :: "[i, i => o] => i"
   53.30 +  PrimReplace :: [i, [i, i] => o] => i
   53.31 +  Replace     :: [i, [i, i] => o] => i
   53.32 +  RepFun      :: [i, i => i] => i
   53.33 +  Collect     :: [i, i => o] => i
   53.34  
   53.35    (* Descriptions *)
   53.36  
   53.37 -  The         :: "(i => o) => i"      (binder "THE " 10)
   53.38 -  if          :: "[o, i, i] => i"
   53.39 +  The         :: (i => o) => i      (binder "THE " 10)
   53.40 +  if          :: [o, i, i] => i
   53.41  
   53.42    (* Finite Sets *)
   53.43  
   53.44 -  Upair, cons :: "[i, i] => i"
   53.45 -  succ        :: "i => i"
   53.46 +  Upair, cons :: [i, i] => i
   53.47 +  succ        :: i => i
   53.48  
   53.49    (* Ordered Pairing *)
   53.50  
   53.51 -  Pair        :: "[i, i] => i"
   53.52 -  fst, snd    :: "i => i"
   53.53 -  split       :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
   53.54 +  Pair        :: [i, i] => i
   53.55 +  fst, snd    :: i => i
   53.56 +  split       :: [[i, i] => 'a, i] => 'a::logic  (*for pattern-matching*)
   53.57  
   53.58    (* Sigma and Pi Operators *)
   53.59  
   53.60 -  Sigma, Pi   :: "[i, i => i] => i"
   53.61 +  Sigma, Pi   :: [i, i => i] => i
   53.62  
   53.63    (* Relations and Functions *)
   53.64  
   53.65 -  domain      :: "i => i"
   53.66 -  range       :: "i => i"
   53.67 -  field       :: "i => i"
   53.68 -  converse    :: "i => i"
   53.69 -  function    :: "i => o"	    	(*is a relation a function?*)
   53.70 -  Lambda      :: "[i, i => i] => i"
   53.71 -  restrict    :: "[i, i] => i"
   53.72 +  domain      :: i => i
   53.73 +  range       :: i => i
   53.74 +  field       :: i => i
   53.75 +  converse    :: i => i
   53.76 +  function    :: i => o	    	(*is a relation a function?*)
   53.77 +  Lambda      :: [i, i => i] => i
   53.78 +  restrict    :: [i, i] => i
   53.79  
   53.80    (* Infixes in order of decreasing precedence *)
   53.81  
   53.82 -  "``"        :: "[i, i] => i"    (infixl 90) (*image*)
   53.83 -  "-``"       :: "[i, i] => i"    (infixl 90) (*inverse image*)
   53.84 -  "`"         :: "[i, i] => i"    (infixl 90) (*function application*)
   53.85 -(*"*"         :: "[i, i] => i"    (infixr 80) (*Cartesian product*)*)
   53.86 -  "Int"       :: "[i, i] => i"    (infixl 70) (*binary intersection*)
   53.87 -  "Un"        :: "[i, i] => i"    (infixl 65) (*binary union*)
   53.88 -  "-"         :: "[i, i] => i"    (infixl 65) (*set difference*)
   53.89 -(*"->"        :: "[i, i] => i"    (infixr 60) (*function space*)*)
   53.90 -  "<="        :: "[i, i] => o"    (infixl 50) (*subset relation*)
   53.91 -  ":"         :: "[i, i] => o"    (infixl 50) (*membership relation*)
   53.92 -(*"~:"        :: "[i, i] => o"    (infixl 50) (*negated membership relation*)*)
   53.93 +  "``"        :: [i, i] => i    (infixl 90) (*image*)
   53.94 +  "-``"       :: [i, i] => i    (infixl 90) (*inverse image*)
   53.95 +  "`"         :: [i, i] => i    (infixl 90) (*function application*)
   53.96 +(*"*"         :: [i, i] => i    (infixr 80) (*Cartesian product*)*)
   53.97 +  "Int"       :: [i, i] => i    (infixl 70) (*binary intersection*)
   53.98 +  "Un"        :: [i, i] => i    (infixl 65) (*binary union*)
   53.99 +  "-"         :: [i, i] => i    (infixl 65) (*set difference*)
  53.100 +(*"->"        :: [i, i] => i    (infixr 60) (*function space*)*)
  53.101 +  "<="        :: [i, i] => o    (infixl 50) (*subset relation*)
  53.102 +  ":"         :: [i, i] => o    (infixl 50) (*membership relation*)
  53.103 +(*"~:"        :: [i, i] => o    (infixl 50) (*negated membership relation*)*)
  53.104  
  53.105  
  53.106  types
  53.107 @@ -85,29 +85,29 @@
  53.108    pttrns
  53.109  
  53.110  syntax
  53.111 -  ""          :: "i => is"                   ("_")
  53.112 -  "@Enum"     :: "[i, is] => is"             ("_,/ _")
  53.113 -  "~:"        :: "[i, i] => o"               (infixl 50)
  53.114 -  "@Finset"   :: "is => i"                   ("{(_)}")
  53.115 -  "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
  53.116 -  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
  53.117 -  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
  53.118 -  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
  53.119 -  "@INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
  53.120 -  "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
  53.121 -  "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
  53.122 -  "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
  53.123 -  "->"        :: "[i, i] => i"               (infixr 60)
  53.124 -  "*"         :: "[i, i] => i"               (infixr 80)
  53.125 -  "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
  53.126 -  "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
  53.127 -  "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
  53.128 +  ""          :: i => is                   ("_")
  53.129 +  "@Enum"     :: [i, is] => is             ("_,/ _")
  53.130 +  "~:"        :: [i, i] => o               (infixl 50)
  53.131 +  "@Finset"   :: is => i                   ("{(_)}")
  53.132 +  "@Tuple"    :: [i, is] => i              ("<(_,/ _)>")
  53.133 +  "@Collect"  :: [pttrn, i, o] => i        ("(1{_: _ ./ _})")
  53.134 +  "@Replace"  :: [pttrn, pttrn, i, o] => i ("(1{_ ./ _: _, _})")
  53.135 +  "@RepFun"   :: [i, pttrn, i] => i        ("(1{_ ./ _: _})" [51,0,51])
  53.136 +  "@INTER"    :: [pttrn, i, i] => i        ("(3INT _:_./ _)" 10)
  53.137 +  "@UNION"    :: [pttrn, i, i] => i        ("(3UN _:_./ _)" 10)
  53.138 +  "@PROD"     :: [pttrn, i, i] => i        ("(3PROD _:_./ _)" 10)
  53.139 +  "@SUM"      :: [pttrn, i, i] => i        ("(3SUM _:_./ _)" 10)
  53.140 +  "->"        :: [i, i] => i               (infixr 60)
  53.141 +  "*"         :: [i, i] => i               (infixr 80)
  53.142 +  "@lam"      :: [pttrn, i, i] => i        ("(3lam _:_./ _)" 10)
  53.143 +  "@Ball"     :: [pttrn, i, o] => o        ("(3ALL _:_./ _)" 10)
  53.144 +  "@Bex"      :: [pttrn, i, o] => o        ("(3EX _:_./ _)" 10)
  53.145  
  53.146    (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
  53.147  
  53.148 -  "@pttrn"  :: "pttrns => pttrn"            ("<_>")
  53.149 -  ""        :: " pttrn           => pttrns" ("_")
  53.150 -  "@pttrns" :: "[pttrn,pttrns]   => pttrns" ("_,/_")
  53.151 +  "@pttrn"  :: pttrns => pttrn            ("<_>")
  53.152 +  ""        ::  pttrn           => pttrns ("_")
  53.153 +  "@pttrns" :: [pttrn,pttrns]   => pttrns ("_,/_")
  53.154  
  53.155  translations
  53.156    "x ~: y"      == "~ (x : y)"
    54.1 --- a/src/ZF/Zorn.thy	Fri Dec 08 19:48:15 1995 +0100
    54.2 +++ b/src/ZF/Zorn.thy	Sat Dec 09 13:36:11 1995 +0100
    54.3 @@ -14,10 +14,10 @@
    54.4  Zorn = OrderArith + AC + Inductive +
    54.5  
    54.6  consts
    54.7 -  Subset_rel      :: "i=>i"
    54.8 -  increasing      :: "i=>i"
    54.9 -  chain, maxchain :: "i=>i"
   54.10 -  super           :: "[i,i]=>i"
   54.11 +  Subset_rel      :: i=>i
   54.12 +  increasing      :: i=>i
   54.13 +  chain, maxchain :: i=>i
   54.14 +  super           :: [i,i]=>i
   54.15  
   54.16  defs
   54.17    Subset_rel_def "Subset_rel(A) == {z: A*A . EX x y. z=<x,y> & x<=y & x~=y}"
   54.18 @@ -34,7 +34,7 @@
   54.19      are therefore unconditional.
   54.20  **)
   54.21  consts
   54.22 -  "TFin" :: "[i,i]=>i"
   54.23 +  "TFin" :: [i,i]=>i
   54.24  
   54.25  inductive
   54.26    domains       "TFin(S,next)" <= "Pow(S)"
    55.1 --- a/src/ZF/ex/Acc.thy	Fri Dec 08 19:48:15 1995 +0100
    55.2 +++ b/src/ZF/ex/Acc.thy	Sat Dec 09 13:36:11 1995 +0100
    55.3 @@ -12,7 +12,7 @@
    55.4  Acc = WF + Inductive +
    55.5  
    55.6  consts
    55.7 -  acc :: "i=>i"
    55.8 +  acc :: i=>i
    55.9  
   55.10  inductive
   55.11    domains "acc(r)" <= "field(r)"
    56.1 --- a/src/ZF/ex/BT.thy	Fri Dec 08 19:48:15 1995 +0100
    56.2 +++ b/src/ZF/ex/BT.thy	Sat Dec 09 13:36:11 1995 +0100
    56.3 @@ -8,12 +8,12 @@
    56.4  
    56.5  BT = Datatype +
    56.6  consts
    56.7 -    bt_rec    	:: "[i, i, [i,i,i,i,i]=>i] => i"
    56.8 -    n_nodes	:: "i=>i"
    56.9 -    n_leaves   	:: "i=>i"
   56.10 -    bt_reflect 	:: "i=>i"
   56.11 +    bt_rec    	:: [i, i, [i,i,i,i,i]=>i] => i
   56.12 +    n_nodes	:: i=>i
   56.13 +    n_leaves   	:: i=>i
   56.14 +    bt_reflect 	:: i=>i
   56.15  
   56.16 -    bt 	        :: "i=>i"
   56.17 +    bt 	        :: i=>i
   56.18  
   56.19  datatype
   56.20    "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
    57.1 --- a/src/ZF/ex/Bin.thy	Fri Dec 08 19:48:15 1995 +0100
    57.2 +++ b/src/ZF/ex/Bin.thy	Sat Dec 09 13:36:11 1995 +0100
    57.3 @@ -21,18 +21,18 @@
    57.4  Bin = Integ + Datatype + "twos_compl" +
    57.5  
    57.6  consts
    57.7 -  bin_rec          :: "[i, i, i, [i,i,i]=>i] => i"
    57.8 -  integ_of_bin     :: "i=>i"
    57.9 -  norm_Bcons       :: "[i,i]=>i"
   57.10 -  bin_succ         :: "i=>i"
   57.11 -  bin_pred         :: "i=>i"
   57.12 -  bin_minus        :: "i=>i"
   57.13 -  bin_add,bin_mult :: "[i,i]=>i"
   57.14 +  bin_rec          :: [i, i, i, [i,i,i]=>i] => i
   57.15 +  integ_of_bin     :: i=>i
   57.16 +  norm_Bcons       :: [i,i]=>i
   57.17 +  bin_succ         :: i=>i
   57.18 +  bin_pred         :: i=>i
   57.19 +  bin_minus        :: i=>i
   57.20 +  bin_add,bin_mult :: [i,i]=>i
   57.21  
   57.22 -  bin              :: "i"
   57.23 +  bin              :: i
   57.24  
   57.25  syntax
   57.26 -  "_Int"           :: "xnum => i"        ("_")
   57.27 +  "_Int"           :: xnum => i        ("_")
   57.28  
   57.29  datatype
   57.30    "bin" = Plus
    58.1 --- a/src/ZF/ex/Brouwer.thy	Fri Dec 08 19:48:15 1995 +0100
    58.2 +++ b/src/ZF/ex/Brouwer.thy	Sat Dec 09 13:36:11 1995 +0100
    58.3 @@ -10,8 +10,8 @@
    58.4  
    58.5  Brouwer = InfDatatype +
    58.6  consts
    58.7 -  brouwer :: "i"
    58.8 -  Well    :: "[i,i=>i]=>i"
    58.9 +  brouwer :: i
   58.10 +  Well    :: [i,i=>i]=>i
   58.11   
   58.12  datatype <= "Vfrom(0, csucc(nat))"
   58.13    "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
    59.1 --- a/src/ZF/ex/CoUnit.thy	Fri Dec 08 19:48:15 1995 +0100
    59.2 +++ b/src/ZF/ex/CoUnit.thy	Sat Dec 09 13:36:11 1995 +0100
    59.3 @@ -17,7 +17,7 @@
    59.4    Coalgebra Theorem
    59.5  *)
    59.6  consts
    59.7 -  counit :: "i"
    59.8 +  counit :: i
    59.9  codatatype
   59.10    "counit" = Con ("x: counit")
   59.11  
   59.12 @@ -27,7 +27,7 @@
   59.13  *)
   59.14  
   59.15  consts
   59.16 -  counit2 :: "i"
   59.17 +  counit2 :: i
   59.18  codatatype
   59.19    "counit2" = Con2 ("x: counit2", "y: counit2")
   59.20  
    60.1 --- a/src/ZF/ex/Comb.thy	Fri Dec 08 19:48:15 1995 +0100
    60.2 +++ b/src/ZF/ex/Comb.thy	Sat Dec 09 13:36:11 1995 +0100
    60.3 @@ -16,7 +16,7 @@
    60.4  Comb = Datatype +
    60.5  
    60.6  (** Datatype definition of combinators S and K, with infixed application **)
    60.7 -consts comb :: "i"
    60.8 +consts comb :: i
    60.9  datatype (* <= "univ(0)" *)
   60.10    "comb" = K
   60.11           | S
   60.12 @@ -26,9 +26,9 @@
   60.13               and (multi-step) reductions, --->
   60.14  **)
   60.15  consts
   60.16 -  contract  :: "i"
   60.17 -  "-1->"    :: "[i,i] => o"    			(infixl 50)
   60.18 -  "--->"    :: "[i,i] => o"    			(infixl 50)
   60.19 +  contract  :: i
   60.20 +  "-1->"    :: [i,i] => o    			(infixl 50)
   60.21 +  "--->"    :: [i,i] => o    			(infixl 50)
   60.22  
   60.23  translations
   60.24    "p -1-> q" == "<p,q> : contract"
   60.25 @@ -48,9 +48,9 @@
   60.26               and (multi-step) parallel reductions, ===>
   60.27  **)
   60.28  consts
   60.29 -  parcontract :: "i"
   60.30 -  "=1=>"    :: "[i,i] => o"    			(infixl 50)
   60.31 -  "===>"    :: "[i,i] => o"    			(infixl 50)
   60.32 +  parcontract :: i
   60.33 +  "=1=>"    :: [i,i] => o    			(infixl 50)
   60.34 +  "===>"    :: [i,i] => o    			(infixl 50)
   60.35  
   60.36  translations
   60.37    "p =1=> q" == "<p,q> : parcontract"
   60.38 @@ -68,8 +68,8 @@
   60.39  
   60.40  (*Misc definitions*)
   60.41  consts
   60.42 -  diamond   :: "i => o"
   60.43 -  I         :: "i"
   60.44 +  diamond   :: i => o
   60.45 +  I         :: i
   60.46  
   60.47  defs
   60.48  
    61.1 --- a/src/ZF/ex/Data.thy	Fri Dec 08 19:48:15 1995 +0100
    61.2 +++ b/src/ZF/ex/Data.thy	Sat Dec 09 13:36:11 1995 +0100
    61.3 @@ -10,7 +10,7 @@
    61.4  Data = Datatype +
    61.5  
    61.6  consts
    61.7 -  data :: "[i,i] => i"
    61.8 +  data :: [i,i] => i
    61.9  
   61.10  datatype
   61.11    "data(A,B)" = Con0
    62.1 --- a/src/ZF/ex/Enum.thy	Fri Dec 08 19:48:15 1995 +0100
    62.2 +++ b/src/ZF/ex/Enum.thy	Sat Dec 09 13:36:11 1995 +0100
    62.3 @@ -11,7 +11,7 @@
    62.4  Enum = Datatype + 
    62.5  
    62.6  consts
    62.7 -  enum :: "i"
    62.8 +  enum :: i
    62.9  
   62.10  datatype
   62.11    "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
    63.1 --- a/src/ZF/ex/Integ.thy	Fri Dec 08 19:48:15 1995 +0100
    63.2 +++ b/src/ZF/ex/Integ.thy	Sat Dec 09 13:36:11 1995 +0100
    63.3 @@ -8,17 +8,17 @@
    63.4  
    63.5  Integ = EquivClass + Arith +
    63.6  consts
    63.7 -    intrel,integ::      "i"
    63.8 -    znat	::	"i=>i"		("$# _" [80] 80)
    63.9 -    zminus	::	"i=>i"		("$~ _" [80] 80)
   63.10 -    znegative	::	"i=>o"
   63.11 -    zmagnitude	::	"i=>i"
   63.12 -    "$*"        ::      "[i,i]=>i"      (infixl 70)
   63.13 -    "$'/"       ::      "[i,i]=>i"      (infixl 70) 
   63.14 -    "$'/'/"     ::      "[i,i]=>i"      (infixl 70)
   63.15 -    "$+"	::      "[i,i]=>i"      (infixl 65)
   63.16 -    "$-"        ::      "[i,i]=>i"      (infixl 65)
   63.17 -    "$<"	:: 	"[i,i]=>o"  	(infixl 50)
   63.18 +    intrel,integ::      i
   63.19 +    znat	::	i=>i		("$# _" [80] 80)
   63.20 +    zminus	::	i=>i		("$~ _" [80] 80)
   63.21 +    znegative	::	i=>o
   63.22 +    zmagnitude	::	i=>i
   63.23 +    "$*"        ::      [i,i]=>i      (infixl 70)
   63.24 +    "$'/"       ::      [i,i]=>i      (infixl 70) 
   63.25 +    "$'/'/"     ::      [i,i]=>i      (infixl 70)
   63.26 +    "$+"	::      [i,i]=>i      (infixl 65)
   63.27 +    "$-"        ::      [i,i]=>i      (infixl 65)
   63.28 +    "$<"	:: 	[i,i]=>o  	(infixl 50)
   63.29  
   63.30  defs
   63.31  
    64.1 --- a/src/ZF/ex/LList.thy	Fri Dec 08 19:48:15 1995 +0100
    64.2 +++ b/src/ZF/ex/LList.thy	Sat Dec 09 13:36:11 1995 +0100
    64.3 @@ -17,7 +17,7 @@
    64.4  LList = Datatype +
    64.5  
    64.6  consts
    64.7 -  llist  :: "i=>i"
    64.8 +  llist  :: i=>i
    64.9  
   64.10  codatatype
   64.11    "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
   64.12 @@ -25,7 +25,7 @@
   64.13  
   64.14  (*Coinductive definition of equality*)
   64.15  consts
   64.16 -  lleq :: "i=>i"
   64.17 +  lleq :: i=>i
   64.18  
   64.19  (*Previously used <*> in the domain and variant pairs as elements.  But
   64.20    standard pairs work just as well.  To use variant pairs, must change prefix
   64.21 @@ -40,8 +40,8 @@
   64.22  
   64.23  (*Lazy list functions; flip is not definitional!*)
   64.24  consts
   64.25 -  lconst   :: "i => i"
   64.26 -  flip     :: "i => i"
   64.27 +  lconst   :: i => i
   64.28 +  flip     :: i => i
   64.29  
   64.30  defs
   64.31    lconst_def  "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
    65.1 --- a/src/ZF/ex/Limit.thy	Fri Dec 08 19:48:15 1995 +0100
    65.2 +++ b/src/ZF/ex/Limit.thy	Sat Dec 09 13:36:11 1995 +0100
    65.3 @@ -21,43 +21,43 @@
    65.4  
    65.5  consts
    65.6  
    65.7 -  "rel" :: "[i,i,i]=>o"                 (* rel(D,x,y) *)
    65.8 -  "set" :: "i=>i"                       (* set(D) *)
    65.9 -  "po"  :: "i=>o"                       (* po(D) *)
   65.10 -  "chain" :: "[i,i]=>o"                 (* chain(D,X) *)
   65.11 -  "isub" :: "[i,i,i]=>o"                (* isub(D,X,x) *)
   65.12 -  "islub" :: "[i,i,i]=>o"               (* islub(D,X,x) *)
   65.13 -  "lub" :: "[i,i]=>i"                   (* lub(D,X) *)
   65.14 -  "cpo" :: "i=>o"                       (* cpo(D) *)
   65.15 -  "pcpo" :: "i=>o"                      (* pcpo(D) *)
   65.16 -  "bot" :: "i=>i"                       (* bot(D) *)
   65.17 -  "mono" :: "[i,i]=>i"                  (* mono(D,E) *)
   65.18 -  "cont" :: "[i,i]=>i"                  (* cont(D,E) *)
   65.19 -  "cf" :: "[i,i]=>i"                    (* cf(D,E) *)
   65.20 +  "rel" :: [i,i,i]=>o                 (* rel(D,x,y) *)
   65.21 +  "set" :: i=>i                       (* set(D) *)
   65.22 +  "po"  :: i=>o                       (* po(D) *)
   65.23 +  "chain" :: [i,i]=>o                 (* chain(D,X) *)
   65.24 +  "isub" :: [i,i,i]=>o                (* isub(D,X,x) *)
   65.25 +  "islub" :: [i,i,i]=>o               (* islub(D,X,x) *)
   65.26 +  "lub" :: [i,i]=>i                   (* lub(D,X) *)
   65.27 +  "cpo" :: i=>o                       (* cpo(D) *)
   65.28 +  "pcpo" :: i=>o                      (* pcpo(D) *)
   65.29 +  "bot" :: i=>i                       (* bot(D) *)
   65.30 +  "mono" :: [i,i]=>i                  (* mono(D,E) *)
   65.31 +  "cont" :: [i,i]=>i                  (* cont(D,E) *)
   65.32 +  "cf" :: [i,i]=>i                    (* cf(D,E) *)
   65.33  
   65.34 -  "suffix" :: "[i,i]=>i"                (* suffix(X,n) *)
   65.35 -  "subchain" :: "[i,i]=>o"              (* subchain(X,Y) *)
   65.36 -  "dominate" :: "[i,i,i]=>o"            (* dominate(D,X,Y) *)
   65.37 -  "matrix" :: "[i,i]=>o"                (* matrix(D,M) *)
   65.38 +  "suffix" :: [i,i]=>i                (* suffix(X,n) *)
   65.39 +  "subchain" :: [i,i]=>o              (* subchain(X,Y) *)
   65.40 +  "dominate" :: [i,i,i]=>o            (* dominate(D,X,Y) *)
   65.41 +  "matrix" :: [i,i]=>o                (* matrix(D,M) *)
   65.42  
   65.43 -  "projpair"  :: "[i,i,i,i]=>o"         (* projpair(D,E,e,p) *)
   65.44 -  "emb"       :: "[i,i,i]=>o"           (* emb(D,E,e) *)
   65.45 -  "Rp"        :: "[i,i,i]=>i"           (* Rp(D,E,e) *)
   65.46 -  "iprod"     :: "i=>i"                 (* iprod(DD) *)
   65.47 -  "mkcpo"     :: "[i,i=>o]=>i"          (* mkcpo(D,P) *)
   65.48 -  "subcpo"    :: "[i,i]=>o"             (* subcpo(D,E) *)
   65.49 -  "subpcpo"   :: "[i,i]=>o"             (* subpcpo(D,E) *)
   65.50 +  "projpair"  :: [i,i,i,i]=>o         (* projpair(D,E,e,p) *)
   65.51 +  "emb"       :: [i,i,i]=>o           (* emb(D,E,e) *)
   65.52 +  "Rp"        :: [i,i,i]=>i           (* Rp(D,E,e) *)
   65.53 +  "iprod"     :: i=>i                 (* iprod(DD) *)
   65.54 +  "mkcpo"     :: [i,i=>o]=>i          (* mkcpo(D,P) *)
   65.55 +  "subcpo"    :: [i,i]=>o             (* subcpo(D,E) *)
   65.56 +  "subpcpo"   :: [i,i]=>o             (* subpcpo(D,E) *)
   65.57  
   65.58 -  "emb_chain" :: "[i,i]=>o"             (* emb_chain(DD,ee) *)
   65.59 -  "Dinf"      :: "[i,i]=>i"             (* Dinf(DD,ee) *)
   65.60 +  "emb_chain" :: [i,i]=>o             (* emb_chain(DD,ee) *)
   65.61 +  "Dinf"      :: [i,i]=>i             (* Dinf(DD,ee) *)
   65.62  
   65.63 -  "e_less"    :: "[i,i,i,i]=>i"         (* e_less(DD,ee,m,n) *)
   65.64 -  "e_gr"      :: "[i,i,i,i]=>i"         (* e_gr(DD,ee,m,n) *)
   65.65 -  "eps"       :: "[i,i,i,i]=>i"         (* eps(DD,ee,m,n) *)
   65.66 -  "rho_emb"   :: "[i,i,i]=>i"           (* rho_emb(DD,ee,n) *)
   65.67 -  "rho_proj"  :: "[i,i,i]=>i"           (* rho_proj(DD,ee,n) *)
   65.68 -  "commute"   :: "[i,i,i,i=>i]=>o"      (* commute(DD,ee,E,r) *)
   65.69 -  "mediating" :: "[i,i,i=>i,i=>i,i]=>o" (* mediating(E,G,r,f,t) *)
   65.70 +  "e_less"    :: [i,i,i,i]=>i         (* e_less(DD,ee,m,n) *)
   65.71 +  "e_gr"      :: [i,i,i,i]=>i         (* e_gr(DD,ee,m,n) *)
   65.72 +  "eps"       :: [i,i,i,i]=>i         (* eps(DD,ee,m,n) *)
   65.73 +  "rho_emb"   :: [i,i,i]=>i           (* rho_emb(DD,ee,n) *)
   65.74 +  "rho_proj"  :: [i,i,i]=>i           (* rho_proj(DD,ee,n) *)
   65.75 +  "commute"   :: [i,i,i,i=>i]=>o      (* commute(DD,ee,E,r) *)
   65.76 +  "mediating" :: [i,i,i=>i,i=>i,i]=>o (* mediating(E,G,r,f,t) *)
   65.77  
   65.78  rules
   65.79  
    66.1 --- a/src/ZF/ex/ListN.thy	Fri Dec 08 19:48:15 1995 +0100
    66.2 +++ b/src/ZF/ex/ListN.thy	Sat Dec 09 13:36:11 1995 +0100
    66.3 @@ -10,7 +10,7 @@
    66.4  *)
    66.5  
    66.6  ListN = List +
    66.7 -consts	listn ::"i=>i"
    66.8 +consts	listn ::i=>i
    66.9  inductive
   66.10    domains   "listn(A)" <= "nat*list(A)"
   66.11    intrs
    67.1 --- a/src/ZF/ex/Ntree.thy	Fri Dec 08 19:48:15 1995 +0100
    67.2 +++ b/src/ZF/ex/Ntree.thy	Sat Dec 09 13:36:11 1995 +0100
    67.3 @@ -11,9 +11,9 @@
    67.4  
    67.5  Ntree = InfDatatype +
    67.6  consts
    67.7 -  ntree    :: "i=>i"
    67.8 -  maptree  :: "i=>i"
    67.9 -  maptree2 :: "[i,i] => i"
   67.10 +  ntree    :: i=>i
   67.11 +  maptree  :: i=>i
   67.12 +  maptree2 :: [i,i] => i
   67.13  
   67.14  datatype
   67.15    "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
    68.1 --- a/src/ZF/ex/Primrec.thy	Fri Dec 08 19:48:15 1995 +0100
    68.2 +++ b/src/ZF/ex/Primrec.thy	Sat Dec 09 13:36:11 1995 +0100
    68.3 @@ -16,14 +16,14 @@
    68.4  
    68.5  Primrec = List +
    68.6  consts
    68.7 -    primrec :: "i"
    68.8 -    SC      :: "i"
    68.9 -    CONST   :: "i=>i"
   68.10 -    PROJ    :: "i=>i"
   68.11 -    COMP    :: "[i,i]=>i"
   68.12 -    PREC    :: "[i,i]=>i"
   68.13 -    ACK	    :: "i=>i"
   68.14 -    ack	    :: "[i,i]=>i"
   68.15 +    primrec :: i
   68.16 +    SC      :: i
   68.17 +    CONST   :: i=>i
   68.18 +    PROJ    :: i=>i
   68.19 +    COMP    :: [i,i]=>i
   68.20 +    PREC    :: [i,i]=>i
   68.21 +    ACK	    :: i=>i
   68.22 +    ack	    :: [i,i]=>i
   68.23  
   68.24  translations
   68.25    "ack(x,y)"  == "ACK(x) ` [y]"
    69.1 --- a/src/ZF/ex/PropLog.thy	Fri Dec 08 19:48:15 1995 +0100
    69.2 +++ b/src/ZF/ex/PropLog.thy	Sat Dec 09 13:36:11 1995 +0100
    69.3 @@ -11,7 +11,7 @@
    69.4  
    69.5  (** The datatype of propositions; note mixfix syntax **)
    69.6  consts
    69.7 -  prop     :: "i"
    69.8 +  prop     :: i
    69.9  
   69.10  datatype
   69.11    "prop" = Fls
   69.12 @@ -20,8 +20,8 @@
   69.13  
   69.14  (** The proof system **)
   69.15  consts
   69.16 -  thms     :: "i => i"
   69.17 -  "|-"     :: "[i,i] => o"    			(infixl 50)
   69.18 +  thms     :: i => i
   69.19 +  "|-"     :: [i,i] => o    			(infixl 50)
   69.20  
   69.21  translations
   69.22    "H |- p" == "p : thms(H)"
   69.23 @@ -39,10 +39,10 @@
   69.24  
   69.25  (** The semantics **)
   69.26  consts
   69.27 -  prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
   69.28 -  is_true  :: "[i,i] => o"
   69.29 -  "|="     :: "[i,i] => o"    			(infixl 50)
   69.30 -  hyps     :: "[i,i] => i"
   69.31 +  prop_rec :: [i, i, i=>i, [i,i,i,i]=>i] => i
   69.32 +  is_true  :: [i,i] => o
   69.33 +  "|="     :: [i,i] => o    			(infixl 50)
   69.34 +  hyps     :: [i,i] => i
   69.35  
   69.36  defs
   69.37  
    70.1 --- a/src/ZF/ex/Ramsey.thy	Fri Dec 08 19:48:15 1995 +0100
    70.2 +++ b/src/ZF/ex/Ramsey.thy	Sat Dec 09 13:36:11 1995 +0100
    70.3 @@ -20,9 +20,9 @@
    70.4  
    70.5  Ramsey = Arith +
    70.6  consts
    70.7 -  Symmetric   		:: "i=>o"
    70.8 -  Atleast     		:: "[i,i]=>o"
    70.9 -  Clique,Indept,Ramsey	:: "[i,i,i]=>o"
   70.10 +  Symmetric   		:: i=>o
   70.11 +  Atleast     		:: [i,i]=>o
   70.12 +  Clique,Indept,Ramsey	:: [i,i,i]=>o
   70.13  
   70.14  defs
   70.15  
    71.1 --- a/src/ZF/ex/Rmap.thy	Fri Dec 08 19:48:15 1995 +0100
    71.2 +++ b/src/ZF/ex/Rmap.thy	Sat Dec 09 13:36:11 1995 +0100
    71.3 @@ -9,7 +9,7 @@
    71.4  Rmap = List +
    71.5  
    71.6  consts
    71.7 -  rmap :: "i=>i"
    71.8 +  rmap :: i=>i
    71.9  
   71.10  inductive
   71.11    domains "rmap(r)" <= "list(domain(r))*list(range(r))"
    72.1 --- a/src/ZF/ex/TF.thy	Fri Dec 08 19:48:15 1995 +0100
    72.2 +++ b/src/ZF/ex/TF.thy	Sat Dec 09 13:36:11 1995 +0100
    72.3 @@ -8,14 +8,14 @@
    72.4  
    72.5  TF = List +
    72.6  consts
    72.7 -  TF_rec      :: "[i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i"
    72.8 -  TF_map      :: "[i=>i, i] => i"
    72.9 -  TF_size     :: "i=>i"
   72.10 -  TF_preorder :: "i=>i"
   72.11 -  list_of_TF  :: "i=>i"
   72.12 -  TF_of_list  :: "i=>i"
   72.13 +  TF_rec      :: [i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i
   72.14 +  TF_map      :: [i=>i, i] => i
   72.15 +  TF_size     :: i=>i
   72.16 +  TF_preorder :: i=>i
   72.17 +  list_of_TF  :: i=>i
   72.18 +  TF_of_list  :: i=>i
   72.19  
   72.20 -  tree, forest, tree_forest    :: "i=>i"
   72.21 +  tree, forest, tree_forest    :: i=>i
   72.22  
   72.23  datatype
   72.24    "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
    73.1 --- a/src/ZF/ex/Term.thy	Fri Dec 08 19:48:15 1995 +0100
    73.2 +++ b/src/ZF/ex/Term.thy	Sat Dec 09 13:36:11 1995 +0100
    73.3 @@ -9,13 +9,13 @@
    73.4  
    73.5  Term = List +
    73.6  consts
    73.7 -  term_rec  :: "[i, [i,i,i]=>i] => i"
    73.8 -  term_map  :: "[i=>i, i] => i"
    73.9 -  term_size :: "i=>i"
   73.10 -  reflect   :: "i=>i"
   73.11 -  preorder  :: "i=>i"
   73.12 +  term_rec  :: [i, [i,i,i]=>i] => i
   73.13 +  term_map  :: [i=>i, i] => i
   73.14 +  term_size :: i=>i
   73.15 +  reflect   :: i=>i
   73.16 +  preorder  :: i=>i
   73.17  
   73.18 -  term      :: "i=>i"
   73.19 +  term      :: i=>i
   73.20  
   73.21  datatype
   73.22    "term(A)" = Apply ("a: A", "l: list(term(A))")