fixed dots;
authorwenzelm
Fri Oct 10 17:10:12 1997 +0200 (1997-10-10)
changeset 3837d7f033c74b38
parent 3836 f1a1817659e6
child 3838 a16277522928
fixed dots;
src/CCL/CCL.ML
src/CCL/CCL.thy
src/CCL/Fix.ML
src/CCL/Fix.thy
src/CCL/Gfp.ML
src/CCL/Hered.ML
src/CCL/Hered.thy
src/CCL/Lfp.ML
src/CCL/Set.ML
src/CCL/Set.thy
src/CCL/Term.ML
src/CCL/Term.thy
src/CCL/Type.ML
src/CCL/Type.thy
src/CCL/Wfd.ML
src/CCL/Wfd.thy
src/CCL/coinduction.ML
src/CCL/equalities.ML
src/CCL/eval.ML
src/CCL/ex/Flag.thy
src/CCL/ex/List.ML
src/CCL/ex/List.thy
src/CCL/ex/Nat.thy
src/CCL/ex/Stream.ML
src/CCL/genrec.ML
src/CCL/subset.ML
src/CCL/typecheck.ML
src/CTT/Arith.ML
src/CTT/Arith.thy
src/CTT/Bool.thy
src/CTT/CTT.ML
src/CTT/CTT.thy
src/CTT/ex/elim.ML
src/CTT/ex/equal.ML
src/CTT/ex/typechk.ML
src/LCF/LCF.ML
src/LCF/LCF.thy
src/LCF/fix.ML
     1.1 --- a/src/CCL/CCL.ML	Fri Oct 10 16:29:41 1997 +0200
     1.2 +++ b/src/CCL/CCL.ML	Fri Oct 10 17:10:12 1997 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
     1.5   (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
     1.6  
     1.7 -goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x.f(x)) = (%x.g(x))";
     1.8 +goal CCL.thy  "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
     1.9  by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
    1.10  by (fast_tac (set_cs addIs [po_abstractn]) 1);
    1.11  bind_thm("abstractn", standard (allI RS (result() RS mp)));
    1.12 @@ -68,7 +68,7 @@
    1.13  
    1.14  val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
    1.15                 ["<a,b> = <a',b'> <-> (a=a' & b=b')",
    1.16 -                "(lam x.b(x) = lam x.b'(x)) <-> ((ALL z.b(z)=b'(z)))"];
    1.17 +                "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"];
    1.18  
    1.19  val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE;
    1.20  
    1.21 @@ -140,13 +140,13 @@
    1.22  by (resolve_tac (prems RL [major RS ssubst]) 1);
    1.23  qed "XHlemma1";
    1.24  
    1.25 -goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p.EX t t'.p=<t,t'> &  P(t,t')} <-> Q)";
    1.26 +goal CCL.thy "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> &  P(t,t')} <-> Q)";
    1.27  by (fast_tac ccl_cs 1);
    1.28  bind_thm("XHlemma2", result() RS mp);
    1.29  
    1.30  (*** Pre-Order ***)
    1.31  
    1.32 -goalw CCL.thy [POgen_def,SIM_def]  "mono(%X.POgen(X))";
    1.33 +goalw CCL.thy [POgen_def,SIM_def]  "mono(%X. POgen(X))";
    1.34  by (rtac monoI 1);
    1.35  by (safe_tac ccl_cs);
    1.36  by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
    1.37 @@ -156,15 +156,15 @@
    1.38  
    1.39  goalw CCL.thy [POgen_def,SIM_def]
    1.40    "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
    1.41 -\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
    1.42 -\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
    1.43 +\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
    1.44 +\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
    1.45  by (rtac (iff_refl RS XHlemma2) 1);
    1.46  qed "POgenXH";
    1.47  
    1.48  goal CCL.thy
    1.49    "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
    1.50 -\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
    1.51 -\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x) [= f'(x)))";
    1.52 +\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
    1.53 +\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
    1.54  by (simp_tac (ccl_ss addsimps [PO_iff]) 1);
    1.55  br (rewrite_rule [POgen_def,SIM_def] 
    1.56                   (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
    1.57 @@ -189,7 +189,7 @@
    1.58  by (fast_tac ccl_cs 1);
    1.59  qed "po_pair";
    1.60  
    1.61 -goal CCL.thy "lam x.f(x) [= lam x.f'(x) <-> (ALL x. f(x) [= f'(x))";
    1.62 +goal CCL.thy "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
    1.63  by (rtac (poXH RS iff_trans) 1);
    1.64  by (simp_tac ccl_ss 1);
    1.65  by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
    1.66 @@ -200,13 +200,13 @@
    1.67  val ccl_porews = [po_bot,po_pair,po_lam];
    1.68  
    1.69  val [p1,p2,p3,p4,p5] = goal CCL.thy
    1.70 -    "[| t [= t';  a [= a';  b [= b';  !!x y.c(x,y) [= c'(x,y); \
    1.71 -\       !!u.d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
    1.72 +    "[| t [= t';  a [= a';  b [= b';  !!x y. c(x,y) [= c'(x,y); \
    1.73 +\       !!u. d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
    1.74  by (rtac (p1 RS po_cong RS po_trans) 1);
    1.75  by (rtac (p2 RS po_cong RS po_trans) 1);
    1.76  by (rtac (p3 RS po_cong RS po_trans) 1);
    1.77  by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1);
    1.78 -by (res_inst_tac [("f1","%d.case(t',a',b',c',d)")] 
    1.79 +by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] 
    1.80                 (p5 RS po_abstractn RS po_cong RS po_trans) 1);
    1.81  by (rtac po_refl 1);
    1.82  qed "case_pocong";
    1.83 @@ -217,7 +217,7 @@
    1.84  qed "apply_pocong";
    1.85  
    1.86  
    1.87 -val prems = goal CCL.thy "~ lam x.b(x) [= bot";
    1.88 +val prems = goal CCL.thy "~ lam x. b(x) [= bot";
    1.89  by (rtac notI 1);
    1.90  by (dtac bot_poleast 1);
    1.91  by (etac (distinctness RS notE) 1);
    1.92 @@ -230,14 +230,14 @@
    1.93  by (resolve_tac prems 1);
    1.94  qed "po_lemma";
    1.95  
    1.96 -goal CCL.thy "~ <a,b> [= lam x.f(x)";
    1.97 +goal CCL.thy "~ <a,b> [= lam x. f(x)";
    1.98  by (rtac notI 1);
    1.99  by (rtac (npo_lam_bot RS notE) 1);
   1.100  by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
   1.101  by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
   1.102  qed "npo_pair_lam";
   1.103  
   1.104 -goal CCL.thy "~ lam x.f(x) [= <a,b>";
   1.105 +goal CCL.thy "~ lam x. f(x) [= <a,b>";
   1.106  by (rtac notI 1);
   1.107  by (rtac (npo_lam_bot RS notE) 1);
   1.108  by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
   1.109 @@ -252,9 +252,9 @@
   1.110  val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
   1.111              ["~ true [= false",          "~ false [= true",
   1.112               "~ true [= <a,b>",          "~ <a,b> [= true",
   1.113 -             "~ true [= lam x.f(x)","~ lam x.f(x) [= true",
   1.114 +             "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
   1.115              "~ false [= <a,b>",          "~ <a,b> [= false",
   1.116 -            "~ false [= lam x.f(x)","~ lam x.f(x) [= false"];
   1.117 +            "~ false [= lam x. f(x)","~ lam x. f(x) [= false"];
   1.118  
   1.119  (* Coinduction for [= *)
   1.120  
   1.121 @@ -267,7 +267,7 @@
   1.122  
   1.123  (*************** EQUALITY *******************)
   1.124  
   1.125 -goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X.EQgen(X))";
   1.126 +goalw CCL.thy [EQgen_def,SIM_def]  "mono(%X. EQgen(X))";
   1.127  by (rtac monoI 1);
   1.128  by (safe_tac set_cs);
   1.129  by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
   1.130 @@ -278,19 +278,19 @@
   1.131  goalw CCL.thy [EQgen_def,SIM_def]
   1.132    "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
   1.133  \                                            (t=false & t'=false) | \
   1.134 -\                (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
   1.135 -\                (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))";
   1.136 +\                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
   1.137 +\                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))";
   1.138  by (rtac (iff_refl RS XHlemma2) 1);
   1.139  qed "EQgenXH";
   1.140  
   1.141  goal CCL.thy
   1.142    "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
   1.143 -\                    (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
   1.144 -\                    (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.f(x)=f'(x)))";
   1.145 +\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
   1.146 +\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))";
   1.147  by (subgoal_tac
   1.148    "<t,t'> : EQ <-> (t=bot & t'=bot)  | (t=true & t'=true) | (t=false & t'=false) | \
   1.149 -\             (EX a a' b b'.t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
   1.150 -\             (EX f f'.t=lam x.f(x) &  t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : EQ))" 1);
   1.151 +\             (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
   1.152 +\             (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
   1.153  by (etac rev_mp 1);
   1.154  by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
   1.155  br (rewrite_rule [EQgen_def,SIM_def]
   1.156 @@ -304,7 +304,7 @@
   1.157  qed "eq_coinduct";
   1.158  
   1.159  val prems = goal CCL.thy 
   1.160 -    "[|  <t,u> : R;  R <= EQgen(lfp(%x.EQgen(x) Un R Un EQ)) |] ==> t = u";
   1.161 +    "[|  <t,u> : R;  R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u";
   1.162  by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
   1.163  by (REPEAT (ares_tac (EQgen_mono::prems) 1));
   1.164  qed "eq_coinduct3";
   1.165 @@ -314,18 +314,18 @@
   1.166  
   1.167  (*** Untyped Case Analysis and Other Facts ***)
   1.168  
   1.169 -goalw CCL.thy [apply_def]  "(EX f.t=lam x.f(x)) --> t = lam x.(t ` x)";
   1.170 +goalw CCL.thy [apply_def]  "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
   1.171  by (safe_tac ccl_cs);
   1.172  by (simp_tac ccl_ss 1);
   1.173  bind_thm("cond_eta", result() RS mp);
   1.174  
   1.175 -goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b.t=<a,b>) | (EX f.t=lam x.f(x))";
   1.176 +goal CCL.thy "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
   1.177  by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
   1.178  by (fast_tac set_cs 1);
   1.179  qed "exhaustion";
   1.180  
   1.181  val prems = goal CCL.thy 
   1.182 -    "[| P(bot);  P(true);  P(false);  !!x y.P(<x,y>);  !!b.P(lam x.b(x)) |] ==> P(t)";
   1.183 +    "[| P(bot);  P(true);  P(false);  !!x y. P(<x,y>);  !!b. P(lam x. b(x)) |] ==> P(t)";
   1.184  by (cut_facts_tac [exhaustion] 1);
   1.185  by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
   1.186  qed "term_case";
     2.1 --- a/src/CCL/CCL.thy	Fri Oct 10 16:29:41 1997 +0200
     2.2 +++ b/src/CCL/CCL.thy	Fri Oct 10 17:10:12 1997 +0200
     2.3 @@ -56,18 +56,18 @@
     2.4    trueV       "true ---> true"
     2.5    falseV      "false ---> false"
     2.6    pairV       "<a,b> ---> <a,b>"
     2.7 -  lamV        "lam x.b(x) ---> lam x.b(x)"
     2.8 +  lamV        "lam x. b(x) ---> lam x. b(x)"
     2.9    caseVtrue   "[| t ---> true;  d ---> c |] ==> case(t,d,e,f,g) ---> c"
    2.10    caseVfalse  "[| t ---> false;  e ---> c |] ==> case(t,d,e,f,g) ---> c"
    2.11    caseVpair   "[| t ---> <a,b>;  f(a,b) ---> c |] ==> case(t,d,e,f,g) ---> c"
    2.12 -  caseVlam    "[| t ---> lam x.b(x);  g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
    2.13 +  caseVlam    "[| t ---> lam x. b(x);  g(b) ---> c |] ==> case(t,d,e,f,g) ---> c"
    2.14  
    2.15    (*** Properties of evaluation: note that "t ---> c" impies that c is canonical ***)
    2.16  
    2.17    canonical  "[| t ---> c; c==true ==> u--->v; 
    2.18                            c==false ==> u--->v; 
    2.19 -                    !!a b.c==<a,b> ==> u--->v; 
    2.20 -                      !!f.c==lam x.f(x) ==> u--->v |] ==> 
    2.21 +                    !!a b. c==<a,b> ==> u--->v; 
    2.22 +                      !!f. c==lam x. f(x) ==> u--->v |] ==> 
    2.23               u--->v"
    2.24  
    2.25    (* Should be derivable - but probably a bitch! *)
    2.26 @@ -77,9 +77,9 @@
    2.27  
    2.28    (*** Definitions used in the following rules ***)
    2.29  
    2.30 -  apply_def     "f ` t == case(f,bot,bot,%x y.bot,%u.u(t))"
    2.31 -  bot_def         "bot == (lam x.x`x)`(lam x.x`x)"
    2.32 -  fix_def      "fix(f) == (lam x.f(x`x))`(lam x.f(x`x))"
    2.33 +  apply_def     "f ` t == case(f,bot,bot,%x y. bot,%u. u(t))"
    2.34 +  bot_def         "bot == (lam x. x`x)`(lam x. x`x)"
    2.35 +  fix_def      "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
    2.36  
    2.37    (*  The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
    2.38    (*  as a bisimulation.  They can both be expressed as (bi)simulations up to        *)
    2.39 @@ -87,8 +87,8 @@
    2.40  
    2.41    SIM_def
    2.42    "SIM(t,t',R) ==  (t=true & t'=true) | (t=false & t'=false) | 
    2.43 -                  (EX a a' b b'.t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | 
    2.44 -                  (EX f f'.t=lam x.f(x) & t'=lam x.f'(x) & (ALL x.<f(x),f'(x)> : R))"
    2.45 +                  (EX a a' b b'. t=<a,b> & t'=<a',b'> & <a,a'> : R & <b,b'> : R) | 
    2.46 +                  (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))"
    2.47  
    2.48    POgen_def  "POgen(R) == {p. EX t t'. p=<t,t'> & (t = bot | SIM(t,t',R))}"
    2.49    EQgen_def  "EQgen(R) == {p. EX t t'. p=<t,t'> & (t = bot & t' = bot | SIM(t,t',R))}"
    2.50 @@ -105,7 +105,7 @@
    2.51    po_cong        "a [= b ==> f(a) [= f(b)"
    2.52  
    2.53    (* Extend definition of [= to program fragments of higher type *)
    2.54 -  po_abstractn   "(!!x. f(x) [= g(x)) ==> (%x.f(x)) [= (%x.g(x))"
    2.55 +  po_abstractn   "(!!x. f(x) [= g(x)) ==> (%x. f(x)) [= (%x. g(x))"
    2.56  
    2.57    (** Equality - equivalence axioms inherited from FOL.thy   **)
    2.58    (**          - congruence of "=" is axiomatised implicitly **)
    2.59 @@ -122,11 +122,11 @@
    2.60    caseBtrue            "case(true,d,e,f,g) = d"
    2.61    caseBfalse          "case(false,d,e,f,g) = e"
    2.62    caseBpair           "case(<a,b>,d,e,f,g) = f(a,b)"
    2.63 -  caseBlam       "case(lam x.b(x),d,e,f,g) = g(b)"
    2.64 +  caseBlam       "case(lam x. b(x),d,e,f,g) = g(b)"
    2.65    caseBbot              "case(bot,d,e,f,g) = bot"            (* strictness *)
    2.66  
    2.67    (** The theory is non-trivial **)
    2.68 -  distinctness   "~ lam x.b(x) = bot"
    2.69 +  distinctness   "~ lam x. b(x) = bot"
    2.70  
    2.71    (*** Definitions of Termination and Divergence ***)
    2.72  
     3.1 --- a/src/CCL/Fix.ML	Fri Oct 10 16:29:41 1997 +0200
     3.2 +++ b/src/CCL/Fix.ML	Fri Oct 10 17:10:12 1997 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  (*** Fixed Point Induction ***)
     3.5  
     3.6  val [base,step,incl] = goalw Fix.thy [INCL_def]
     3.7 -    "[| P(bot);  !!x.P(x) ==> P(f(x));  INCL(P) |] ==> P(fix(f))";
     3.8 +    "[| P(bot);  !!x. P(x) ==> P(f(x));  INCL(P) |] ==> P(fix(f))";
     3.9  by (rtac (incl RS spec RS mp) 1);
    3.10  by (rtac (Nat_ind RS ballI) 1 THEN atac 1);
    3.11  by (ALLGOALS (simp_tac term_ss));
    3.12 @@ -26,18 +26,18 @@
    3.13  qed "inclXH";
    3.14  
    3.15  val prems = goal Fix.thy
    3.16 -     "[| !!f.ALL n:Nat.P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x.P(x))";
    3.17 +     "[| !!f. ALL n:Nat. P(f^n`bot) ==> P(fix(f)) |] ==> INCL(%x. P(x))";
    3.18  by (fast_tac (term_cs addIs (prems @ [XH_to_I inclXH])) 1);
    3.19  qed "inclI";
    3.20  
    3.21  val incl::prems = goal Fix.thy
    3.22 -     "[| INCL(P);  !!n.n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
    3.23 +     "[| INCL(P);  !!n. n:Nat ==> P(f^n`bot) |] ==> P(fix(f))";
    3.24  by (fast_tac (term_cs addIs ([ballI RS (incl RS (XH_to_D inclXH) RS spec RS mp)] 
    3.25                         @ prems)) 1);
    3.26  qed "inclD";
    3.27  
    3.28  val incl::prems = goal Fix.thy
    3.29 -     "[| INCL(P);  (ALL n:Nat.P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
    3.30 +     "[| INCL(P);  (ALL n:Nat. P(f^n`bot))-->P(fix(f)) ==> R |] ==> R";
    3.31  by (fast_tac (term_cs addIs ([incl RS inclD] @ prems)) 1);
    3.32  qed "inclE";
    3.33  
    3.34 @@ -55,19 +55,19 @@
    3.35  by (rtac po_cong 1 THEN rtac po_bot 1);
    3.36  qed "npo_INCL";
    3.37  
    3.38 -val prems = goal Fix.thy "[| INCL(P);  INCL(Q) |] ==> INCL(%x.P(x) & Q(x))";
    3.39 +val prems = goal Fix.thy "[| INCL(P);  INCL(Q) |] ==> INCL(%x. P(x) & Q(x))";
    3.40  by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    3.41  qed "conj_INCL";
    3.42  
    3.43 -val prems = goal Fix.thy "[| !!a.INCL(P(a)) |] ==> INCL(%x.ALL a.P(a,x))";
    3.44 +val prems = goal Fix.thy "[| !!a. INCL(P(a)) |] ==> INCL(%x. ALL a. P(a,x))";
    3.45  by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    3.46  qed "all_INCL";
    3.47  
    3.48 -val prems = goal Fix.thy "[| !!a.a:A ==> INCL(P(a)) |] ==> INCL(%x.ALL a:A.P(a,x))";
    3.49 +val prems = goal Fix.thy "[| !!a. a:A ==> INCL(P(a)) |] ==> INCL(%x. ALL a:A. P(a,x))";
    3.50  by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
    3.51  qed "ball_INCL";
    3.52  
    3.53 -goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))";
    3.54 +goal Fix.thy "INCL(%x. a(x) = (b(x)::'a::prog))";
    3.55  by (simp_tac (term_ss addsimps [eq_iff]) 1);
    3.56  by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
    3.57  qed "eq_INCL";
    3.58 @@ -80,7 +80,7 @@
    3.59  by (rtac (fixB RS sym) 1);
    3.60  qed "fix_idgenfp";
    3.61  
    3.62 -goalw Fix.thy [idgen_def] "idgen(lam x.x) = lam x.x";
    3.63 +goalw Fix.thy [idgen_def] "idgen(lam x. x) = lam x. x";
    3.64  by (simp_tac term_ss 1);
    3.65  by (rtac (term_case RS allI) 1);
    3.66  by (ALLGOALS (simp_tac term_ss));
    3.67 @@ -109,14 +109,14 @@
    3.68                 "idgen(d) = d ==> d ` true = true",
    3.69                 "idgen(d) = d ==> d ` false = false",
    3.70                 "idgen(d) = d ==> d ` <a,b> = <d ` a,d ` b>",
    3.71 -               "idgen(d) = d ==> d ` (lam x.f(x)) = lam x.d ` f(x)"]
    3.72 +               "idgen(d) = d ==> d ` (lam x. f(x)) = lam x. d ` f(x)"]
    3.73      end;
    3.74  
    3.75  (* Proof of Reachability law - show that fix and lam x.x both give LEAST fixed points 
    3.76                                 of idgen and hence are they same *)
    3.77  
    3.78  val [p1,p2,p3] = goal CCL.thy
    3.79 -    "[| ALL x.t ` x [= u ` x;  EX f.t=lam x.f(x);  EX f.u=lam x.f(x) |] ==> t [= u";
    3.80 +    "[| ALL x. t ` x [= u ` x;  EX f. t=lam x. f(x);  EX f. u=lam x. f(x) |] ==> t [= u";
    3.81  by (stac (p2 RS cond_eta) 1);
    3.82  by (stac (p3 RS cond_eta) 1);
    3.83  by (rtac (p1 RS (po_lam RS iffD2)) 1);
    3.84 @@ -129,8 +129,8 @@
    3.85  
    3.86  val [prem] = goal Fix.thy
    3.87      "idgen(d) = d ==> \
    3.88 -\      {p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t & b = d ` t)} <=   \
    3.89 -\      POgen({p.EX a b.p=<a,b> & (EX t.a=fix(idgen) ` t  & b = d ` t)})";
    3.90 +\      {p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t & b = d ` t)} <=   \
    3.91 +\      POgen({p. EX a b. p=<a,b> & (EX t. a=fix(idgen) ` t  & b = d ` t)})";
    3.92  by (REPEAT (step_tac term_cs 1));
    3.93  by (term_case_tac "t" 1);
    3.94  by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem,fix_idgenfp] RL idgen_lemmas)))));
    3.95 @@ -146,7 +146,7 @@
    3.96  
    3.97  val [prem] = goal Fix.thy
    3.98      "idgen(d) = d ==> \
    3.99 -\      {p.EX a b.p=<a,b> & b = d ` a} <= POgen({p.EX a b.p=<a,b> & b = d ` a})";
   3.100 +\      {p. EX a b. p=<a,b> & b = d ` a} <= POgen({p. EX a b. p=<a,b> & b = d ` a})";
   3.101  by (REPEAT (step_tac term_cs 1));
   3.102  by (term_case_tac "a" 1);
   3.103  by (ALLGOALS (simp_tac (term_ss addsimps (POgenXH::([prem] RL idgen_lemmas)))));
   3.104 @@ -154,14 +154,14 @@
   3.105  qed "lemma2";
   3.106  
   3.107  val [prem] = goal Fix.thy
   3.108 -    "idgen(d) = d ==> lam x.x [= d";
   3.109 +    "idgen(d) = d ==> lam x. x [= d";
   3.110  by (rtac (allI RS po_eta) 1);
   3.111  by (rtac (lemma2 RSN(2,po_coinduct)) 1);
   3.112  by (simp_tac term_ss 1);
   3.113  by (ALLGOALS (fast_tac (term_cs addIs [prem,po_eta_lemma,fix_idgenfp])));
   3.114  qed "id_least_idgen";
   3.115  
   3.116 -goal Fix.thy  "fix(idgen) = lam x.x";
   3.117 +goal Fix.thy  "fix(idgen) = lam x. x";
   3.118  by (fast_tac (term_cs addIs [eq_iff RS iffD2,
   3.119                               id_idgenfp RS fix_least_idgen,
   3.120                               fix_idgenfp RS id_least_idgen]) 1);
   3.121 @@ -169,7 +169,7 @@
   3.122  
   3.123  (********)
   3.124  
   3.125 -val [prem] = goal Fix.thy "f = lam x.x ==> f`t = t";
   3.126 +val [prem] = goal Fix.thy "f = lam x. x ==> f`t = t";
   3.127  by (rtac (prem RS sym RS subst) 1);
   3.128  by (rtac applyB 1);
   3.129  qed "id_apply";
   3.130 @@ -177,7 +177,7 @@
   3.131  val prems = goal Fix.thy
   3.132       "[| P(bot);  P(true);  P(false);  \
   3.133  \        !!x y.[| P(x);  P(y) |] ==> P(<x,y>);  \
   3.134 -\        !!u.(!!x.P(u(x))) ==> P(lam x.u(x));  INCL(P) |] ==> \
   3.135 +\        !!u.(!!x. P(u(x))) ==> P(lam x. u(x));  INCL(P) |] ==> \
   3.136  \     P(t)";
   3.137  by (rtac (reachability RS id_apply RS subst) 1);
   3.138  by (res_inst_tac [("x","t")] spec 1);
     4.1 --- a/src/CCL/Fix.thy	Fri Oct 10 16:29:41 1997 +0200
     4.2 +++ b/src/CCL/Fix.thy	Fri Oct 10 17:10:12 1997 +0200
     4.3 @@ -17,10 +17,10 @@
     4.4  rules
     4.5  
     4.6    idgen_def
     4.7 -  "idgen(f) == lam t.case(t,true,false,%x y.<f`x, f`y>,%u.lam x.f ` u(x))"
     4.8 +  "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))"
     4.9  
    4.10 -  INCL_def   "INCL(%x.P(x)) == (ALL f.(ALL n:Nat.P(f^n`bot)) --> P(fix(f)))"
    4.11 -  po_INCL    "INCL(%x.a(x) [= b(x))"
    4.12 -  INCL_subst "INCL(P) ==> INCL(%x.P((g::i=>i)(x)))"
    4.13 +  INCL_def   "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))"
    4.14 +  po_INCL    "INCL(%x. a(x) [= b(x))"
    4.15 +  INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))"
    4.16  
    4.17  end
     5.1 --- a/src/CCL/Gfp.ML	Fri Oct 10 16:29:41 1997 +0200
     5.2 +++ b/src/CCL/Gfp.ML	Fri Oct 10 17:10:12 1997 +0200
     5.3 @@ -71,13 +71,13 @@
     5.4           - instead of the condition  A <= f(A)
     5.5                             consider  A <= (f(A) Un f(f(A)) ...) Un gfp(A) ***)
     5.6  
     5.7 -val [prem] = goal Gfp.thy "mono(f) ==> mono(%x.f(x) Un A Un B)";
     5.8 +val [prem] = goal Gfp.thy "mono(f) ==> mono(%x. f(x) Un A Un B)";
     5.9  by (REPEAT (ares_tac [subset_refl, monoI, Un_mono, prem RS monoD] 1));
    5.10  qed "coinduct3_mono_lemma";
    5.11  
    5.12  val [prem,mono] = goal Gfp.thy
    5.13 -    "[| A <= f(lfp(%x.f(x) Un A Un gfp(f)));  mono(f) |] ==> \
    5.14 -\    lfp(%x.f(x) Un A Un gfp(f)) <= f(lfp(%x.f(x) Un A Un gfp(f)))";
    5.15 +    "[| A <= f(lfp(%x. f(x) Un A Un gfp(f)));  mono(f) |] ==> \
    5.16 +\    lfp(%x. f(x) Un A Un gfp(f)) <= f(lfp(%x. f(x) Un A Un gfp(f)))";
    5.17  by (rtac subset_trans 1);
    5.18  by (rtac (mono RS coinduct3_mono_lemma RS lfp_lemma3) 1);
    5.19  by (rtac (Un_least RS Un_least) 1);
    5.20 @@ -90,7 +90,7 @@
    5.21  qed "coinduct3_lemma";
    5.22  
    5.23  val ainA::prems = goal Gfp.thy
    5.24 -    "[| a:A;  A <= f(lfp(%x.f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
    5.25 +    "[| a:A;  A <= f(lfp(%x. f(x) Un A Un gfp(f))); mono(f) |] ==> a : gfp(f)";
    5.26  by (rtac coinduct 1);
    5.27  by (rtac (prems MRS coinduct3_lemma) 2);
    5.28  by (resolve_tac (prems RL [coinduct3_mono_lemma RS lfp_Tarski RS ssubst]) 1);
    5.29 @@ -118,7 +118,7 @@
    5.30  qed "def_coinduct2";
    5.31  
    5.32  val rew::prems = goal Gfp.thy
    5.33 -    "[| h==gfp(f);  a:A;  A <= f(lfp(%x.f(x) Un A Un h)); mono(f) |] ==> a: h";
    5.34 +    "[| h==gfp(f);  a:A;  A <= f(lfp(%x. f(x) Un A Un h)); mono(f) |] ==> a: h";
    5.35  by (rewtac rew);
    5.36  by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems @ [coinduct3]) 1));
    5.37  qed "def_coinduct3";
     6.1 --- a/src/CCL/Hered.ML	Fri Oct 10 16:29:41 1997 +0200
     6.2 +++ b/src/CCL/Hered.ML	Fri Oct 10 17:10:12 1997 +0200
     6.3 @@ -12,20 +12,20 @@
     6.4  
     6.5  (*** Hereditary Termination ***)
     6.6  
     6.7 -goalw Hered.thy [HTTgen_def]  "mono(%X.HTTgen(X))";
     6.8 +goalw Hered.thy [HTTgen_def]  "mono(%X. HTTgen(X))";
     6.9  by (rtac monoI 1);
    6.10  by (fast_tac set_cs 1);
    6.11  qed "HTTgen_mono";
    6.12  
    6.13  goalw Hered.thy [HTTgen_def]
    6.14 -  "t : HTTgen(A) <-> t=true | t=false | (EX a b.t=<a,b> & a : A & b : A) | \
    6.15 -\                                       (EX f.t=lam x.f(x) & (ALL x.f(x) : A))";
    6.16 +  "t : HTTgen(A) <-> t=true | t=false | (EX a b. t=<a,b> & a : A & b : A) | \
    6.17 +\                                       (EX f. t=lam x. f(x) & (ALL x. f(x) : A))";
    6.18  by (fast_tac set_cs 1);
    6.19  qed "HTTgenXH";
    6.20  
    6.21  goal Hered.thy
    6.22 -  "t : HTT <-> t=true | t=false | (EX a b.t=<a,b> & a : HTT & b : HTT) | \
    6.23 -\                                  (EX f.t=lam x.f(x) & (ALL x.f(x) : HTT))";
    6.24 +  "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
    6.25 +\                                  (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
    6.26  br (rewrite_rule [HTTgen_def] 
    6.27                   (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
    6.28  by (fast_tac set_cs 1);
    6.29 @@ -50,7 +50,7 @@
    6.30  by (fast_tac term_cs 1);
    6.31  qed "HTT_pair";
    6.32  
    6.33 -goal Hered.thy "lam x.f(x) : HTT <-> (ALL x. f(x) : HTT)";
    6.34 +goal Hered.thy "lam x. f(x) : HTT <-> (ALL x. f(x) : HTT)";
    6.35  by (rtac (HTTXH RS iff_trans) 1);
    6.36  by (simp_tac term_ss 1);
    6.37  by (safe_tac term_cs);
    6.38 @@ -97,7 +97,7 @@
    6.39         ["true : HTTgen(R)",
    6.40          "false : HTTgen(R)",
    6.41          "[| a : R;  b : R |] ==> <a,b> : HTTgen(R)",
    6.42 -        "[| !!x. b(x) : R |] ==> lam x.b(x) : HTTgen(R)",
    6.43 +        "[| !!x. b(x) : R |] ==> lam x. b(x) : HTTgen(R)",
    6.44          "one : HTTgen(R)",
    6.45          "a : lfp(%x. HTTgen(x) Un R Un HTT) ==> \
    6.46  \                         inl(a) : HTTgen(lfp(%x. HTTgen(x) Un R Un HTT))",
    6.47 @@ -127,7 +127,7 @@
    6.48  qed "PlusF";
    6.49  
    6.50  val prems = goal Hered.thy 
    6.51 -     "[| A <= HTT;  !!x.x:A ==> B(x) <= HTT |] ==> SUM x:A.B(x) <= HTT";
    6.52 +     "[| A <= HTT;  !!x. x:A ==> B(x) <= HTT |] ==> SUM x:A. B(x) <= HTT";
    6.53  by (simp_tac (CCL_ss addsimps ([subsetXH,SgXH] @ HTT_rews)) 1);
    6.54  by (fast_tac (set_cs addIs HTT_Is @ (prems RL [subsetD])) 1);
    6.55  qed "SigmaF";
    6.56 @@ -178,7 +178,7 @@
    6.57  (*** but it seems as easy (and more general) to do this directly by coinduction ***)
    6.58  (*
    6.59  val prems = goal Hered.thy "[| t : HTT;  t [= u |] ==> u [= t";
    6.60 -by (po_coinduct_tac "{p. EX a b.p=<a,b> & b : HTT & b [= a}" 1);
    6.61 +by (po_coinduct_tac "{p. EX a b. p=<a,b> & b : HTT & b [= a}" 1);
    6.62  by (fast_tac (ccl_cs addIs prems) 1);
    6.63  by (safe_tac ccl_cs);
    6.64  by (dtac (poXH RS iffD1) 1);
     7.1 --- a/src/CCL/Hered.thy	Fri Oct 10 16:29:41 1997 +0200
     7.2 +++ b/src/CCL/Hered.thy	Fri Oct 10 17:10:12 1997 +0200
     7.3 @@ -23,8 +23,8 @@
     7.4    (*** Definitions of Hereditary Termination ***)
     7.5  
     7.6    HTTgen_def 
     7.7 -  "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b>      & a : R & b : R) | 
     7.8 -                                      (EX f.  t=lam x.f(x) & (ALL x.f(x) : R))}"
     7.9 +  "HTTgen(R) == {t. t=true | t=false | (EX a b. t=<a,b>      & a : R & b : R) | 
    7.10 +                                      (EX f.  t=lam x. f(x) & (ALL x. f(x) : R))}"
    7.11    HTT_def       "HTT == gfp(HTTgen)"
    7.12  
    7.13  end
     8.1 --- a/src/CCL/Lfp.ML	Fri Oct 10 16:29:41 1997 +0200
     8.2 +++ b/src/CCL/Lfp.ML	Fri Oct 10 17:10:12 1997 +0200
     8.3 @@ -45,7 +45,7 @@
     8.4  
     8.5  val [lfp,mono,indhyp] = goal Lfp.thy
     8.6      "[| a: lfp(f);  mono(f);                            \
     8.7 -\       !!x. [| x: f(lfp(f) Int {x.P(x)}) |] ==> P(x)   \
     8.8 +\       !!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)   \
     8.9  \    |] ==> P(a)";
    8.10  by (res_inst_tac [("a","a")] (Int_lower2 RS subsetD RS CollectD) 1);
    8.11  by (rtac (lfp RSN (2, lfp_lowerbound RS subsetD)) 1);
    8.12 @@ -64,7 +64,7 @@
    8.13  
    8.14  val rew::prems = goal Lfp.thy
    8.15      "[| A == lfp(f);  a:A;  mono(f);                    \
    8.16 -\       !!x. [| x: f(A Int {x.P(x)}) |] ==> P(x)        \
    8.17 +\       !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x)        \
    8.18  \    |] ==> P(a)";
    8.19  by (EVERY1 [rtac induct,        (*backtracking to force correct induction*)
    8.20              REPEAT1 o (ares_tac (map (rewrite_rule [rew]) prems))]);
     9.1 --- a/src/CCL/Set.ML	Fri Oct 10 16:29:41 1997 +0200
     9.2 +++ b/src/CCL/Set.ML	Fri Oct 10 17:10:12 1997 +0200
     9.3 @@ -13,12 +13,12 @@
     9.4  
     9.5  open Set;
     9.6  
     9.7 -val [prem] = goal Set.thy "[| P(a) |] ==> a : {x.P(x)}";
     9.8 +val [prem] = goal Set.thy "[| P(a) |] ==> a : {x. P(x)}";
     9.9  by (rtac (mem_Collect_iff RS iffD2) 1);
    9.10  by (rtac prem 1);
    9.11  qed "CollectI";
    9.12  
    9.13 -val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)";
    9.14 +val prems = goal Set.thy "[| a : {x. P(x)} |] ==> P(a)";
    9.15  by (resolve_tac (prems RL [mem_Collect_iff  RS iffD1]) 1);
    9.16  qed "CollectD";
    9.17  
    9.18 @@ -56,7 +56,7 @@
    9.19  qed "bexI";
    9.20  
    9.21  qed_goal "bexCI" Set.thy 
    9.22 -   "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A.P(x)"
    9.23 +   "[| EX x:A. ~P(x) ==> P(a);  a:A |] ==> EX x:A. P(x)"
    9.24   (fn prems=>
    9.25    [ (rtac classical 1),
    9.26      (REPEAT (ares_tac (prems@[bexI,ballI,notI,notE]) 1))  ]);
    9.27 @@ -93,7 +93,7 @@
    9.28  
    9.29  (*** Rules for subsets ***)
    9.30  
    9.31 -val prems = goalw Set.thy [subset_def] "(!!x.x:A ==> x:B) ==> A <= B";
    9.32 +val prems = goalw Set.thy [subset_def] "(!!x. x:A ==> x:B) ==> A <= B";
    9.33  by (REPEAT (ares_tac (prems @ [ballI]) 1));
    9.34  qed "subsetI";
    9.35  
    9.36 @@ -163,7 +163,7 @@
    9.37  by (REPEAT (resolve_tac (refl::prems) 1));
    9.38  qed "setup_induction";
    9.39  
    9.40 -goal Set.thy "{x.x:A} = A";
    9.41 +goal Set.thy "{x. x:A} = A";
    9.42  by (REPEAT (ares_tac [equalityI,subsetI,CollectI] 1  ORELSE etac CollectD 1));
    9.43  qed "trivial_set";
    9.44  
    9.45 @@ -234,7 +234,7 @@
    9.46  
    9.47  (*** Empty sets ***)
    9.48  
    9.49 -goalw Set.thy [empty_def] "{x.False} = {}";
    9.50 +goalw Set.thy [empty_def] "{x. False} = {}";
    9.51  by (rtac refl 1);
    9.52  qed "empty_eq";
    9.53  
    9.54 @@ -244,7 +244,7 @@
    9.55  
    9.56  val emptyE = make_elim emptyD;
    9.57  
    9.58 -val [prem] = goal Set.thy "~ A={} ==> (EX x.x:A)";
    9.59 +val [prem] = goal Set.thy "~ A={} ==> (EX x. x:A)";
    9.60  by (rtac (prem RS swap) 1);
    9.61  by (rtac equalityI 1);
    9.62  by (ALLGOALS (fast_tac (FOL_cs addSIs [subsetI] addSEs [emptyD])));
    10.1 --- a/src/CCL/Set.thy	Fri Oct 10 16:29:41 1997 +0200
    10.2 +++ b/src/CCL/Set.thy	Fri Oct 10 17:10:12 1997 +0200
    10.3 @@ -50,17 +50,17 @@
    10.4  
    10.5  
    10.6  rules
    10.7 -  mem_Collect_iff       "(a : {x.P(x)}) <-> P(a)"
    10.8 -  set_extension         "A=B <-> (ALL x.x:A <-> x:B)"
    10.9 +  mem_Collect_iff       "(a : {x. P(x)}) <-> P(a)"
   10.10 +  set_extension         "A=B <-> (ALL x. x:A <-> x:B)"
   10.11  
   10.12    Ball_def      "Ball(A, P)  == ALL x. x:A --> P(x)"
   10.13    Bex_def       "Bex(A, P)   == EX x. x:A & P(x)"
   10.14    mono_def      "mono(f)     == (ALL A B. A <= B --> f(A) <= f(B))"
   10.15    subset_def    "A <= B      == ALL x:A. x:B"
   10.16 -  singleton_def "{a}         == {x.x=a}"
   10.17 -  empty_def     "{}          == {x.False}"
   10.18 -  Un_def        "A Un B      == {x.x:A | x:B}"
   10.19 -  Int_def       "A Int B     == {x.x:A & x:B}"
   10.20 +  singleton_def "{a}         == {x. x=a}"
   10.21 +  empty_def     "{}          == {x. False}"
   10.22 +  Un_def        "A Un B      == {x. x:A | x:B}"
   10.23 +  Int_def       "A Int B     == {x. x:A & x:B}"
   10.24    Compl_def     "Compl(A)    == {x. ~x:A}"
   10.25    INTER_def     "INTER(A, B) == {y. ALL x:A. y: B(x)}"
   10.26    UNION_def     "UNION(A, B) == {y. EX x:A. y: B(x)}"
    11.1 --- a/src/CCL/Term.ML	Fri Oct 10 16:29:41 1997 +0200
    11.2 +++ b/src/CCL/Term.ML	Fri Oct 10 17:10:12 1997 +0200
    11.3 @@ -35,7 +35,7 @@
    11.4  by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
    11.5  qed "letBbbot";
    11.6  
    11.7 -goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)";
    11.8 +goalw Term.thy [apply_def] "(lam x. b(x)) ` a = b(a)";
    11.9  by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam])));
   11.10  qed "applyB";
   11.11  
   11.12 @@ -48,7 +48,7 @@
   11.13  qed "fixB";
   11.14  
   11.15  goalw Term.thy [letrec_def]
   11.16 -      "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))";
   11.17 +      "letrec g x be h(x,g) in g(a) = h(a,%y. letrec g x be h(x,g) in g(y))";
   11.18  by (resolve_tac [fixB RS ssubst] 1 THEN 
   11.19      resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1);
   11.20  qed "letrecB";
   11.21 @@ -98,10 +98,10 @@
   11.22  
   11.23  val letrec2B = raw_mk_beta_rl (data_defs @ [letrec2_def])
   11.24         "letrec g x y be h(x,y,g) in g(p,q) = \
   11.25 -\                     h(p,q,%u v.letrec g x y be h(x,y,g) in g(u,v))";
   11.26 +\                     h(p,q,%u v. letrec g x y be h(x,y,g) in g(u,v))";
   11.27  val letrec3B = raw_mk_beta_rl (data_defs @ [letrec3_def])
   11.28         "letrec g x y z be h(x,y,z,g) in g(p,q,r) = \
   11.29 -\                     h(p,q,r,%u v w.letrec g x y z be h(x,y,z,g) in g(u,v,w))";
   11.30 +\                     h(p,q,r,%u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))";
   11.31  
   11.32  val napplyBzero   = mk_beta_rl "f^zero`a = a";
   11.33  val napplyBsucc   = mk_beta_rl "f^succ(n)`a = f(f^n`a)";
    12.1 --- a/src/CCL/Term.thy	Fri Oct 10 16:29:41 1997 +0200
    12.2 +++ b/src/CCL/Term.thy	Fri Oct 10 17:10:12 1997 +0200
    12.3 @@ -54,36 +54,36 @@
    12.4  rules
    12.5  
    12.6    one_def                    "one == true"
    12.7 -  if_def     "if b then t else u  == case(b,t,u,% x y.bot,%v.bot)"
    12.8 +  if_def     "if b then t else u  == case(b,t,u,% x y. bot,%v. bot)"
    12.9    inl_def                 "inl(a) == <true,a>"
   12.10    inr_def                 "inr(b) == <false,b>"
   12.11 -  when_def           "when(t,f,g) == split(t,%b x.if b then f(x) else g(x))"
   12.12 -  split_def           "split(t,f) == case(t,bot,bot,f,%u.bot)"
   12.13 -  fst_def                 "fst(t) == split(t,%x y.x)"
   12.14 -  snd_def                 "snd(t) == split(t,%x y.y)"
   12.15 -  thd_def                 "thd(t) == split(t,%x p.split(p,%y z.z))"
   12.16 +  when_def           "when(t,f,g) == split(t,%b x. if b then f(x) else g(x))"
   12.17 +  split_def           "split(t,f) == case(t,bot,bot,f,%u. bot)"
   12.18 +  fst_def                 "fst(t) == split(t,%x y. x)"
   12.19 +  snd_def                 "snd(t) == split(t,%x y. y)"
   12.20 +  thd_def                 "thd(t) == split(t,%x p. split(p,%y z. z))"
   12.21    zero_def                  "zero == inl(one)"
   12.22    succ_def               "succ(n) == inr(n)"
   12.23 -  ncase_def         "ncase(n,b,c) == when(n,%x.b,%y.c(y))"
   12.24 -  nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)"
   12.25 +  ncase_def         "ncase(n,b,c) == when(n,%x. b,%y. c(y))"
   12.26 +  nrec_def          " nrec(n,b,c) == letrec g x be ncase(x,b,%y. c(y,g(y))) in g(n)"
   12.27    nil_def                     "[] == inl(one)"
   12.28    cons_def                   "h$t == inr(<h,t>)"
   12.29 -  lcase_def         "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))"
   12.30 -  lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)"
   12.31 +  lcase_def         "lcase(l,b,c) == when(l,%x. b,%y. split(y,c))"
   12.32 +  lrec_def           "lrec(l,b,c) == letrec g x be lcase(x,b,%h t. c(h,t,g(t))) in g(l)"
   12.33  
   12.34 -  let_def  "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))"
   12.35 +  let_def  "let x be t in f(x) == case(t,f(true),f(false),%x y. f(<x,y>),%u. f(lam x. u(x)))"
   12.36    letrec_def    
   12.37 -  "letrec g x be h(x,g) in b(g) == b(%x.fix(%f.lam x.h(x,%y.f`y))`x)"
   12.38 +  "letrec g x be h(x,g) in b(g) == b(%x. fix(%f. lam x. h(x,%y. f`y))`x)"
   12.39  
   12.40    letrec2_def  "letrec g x y be h(x,y,g) in f(g)== 
   12.41 -               letrec g' p be split(p,%x y.h(x,y,%u v.g'(<u,v>))) 
   12.42 -                          in f(%x y.g'(<x,y>))"
   12.43 +               letrec g' p be split(p,%x y. h(x,y,%u v. g'(<u,v>))) 
   12.44 +                          in f(%x y. g'(<x,y>))"
   12.45  
   12.46    letrec3_def  "letrec g x y z be h(x,y,z,g) in f(g) == 
   12.47 -             letrec g' p be split(p,%x xs.split(xs,%y z.h(x,y,z,%u v w.g'(<u,<v,w>>)))) 
   12.48 -                          in f(%x y z.g'(<x,<y,z>>))"
   12.49 +             letrec g' p be split(p,%x xs. split(xs,%y z. h(x,y,z,%u v w. g'(<u,<v,w>>)))) 
   12.50 +                          in f(%x y z. g'(<x,<y,z>>))"
   12.51  
   12.52 -  napply_def "f ^n` a == nrec(n,a,%x g.f(g))"
   12.53 +  napply_def "f ^n` a == nrec(n,a,%x g. f(g))"
   12.54  
   12.55  end
   12.56  
    13.1 --- a/src/CCL/Type.ML	Fri Oct 10 16:29:41 1997 +0200
    13.2 +++ b/src/CCL/Type.ML	Fri Oct 10 17:10:12 1997 +0200
    13.3 @@ -15,7 +15,7 @@
    13.4  val simp_data_defs = [one_def,inl_def,inr_def];
    13.5  val ind_data_defs = [zero_def,succ_def,nil_def,cons_def];
    13.6  
    13.7 -goal Set.thy "A <= B <-> (ALL x.x:A --> x:B)";
    13.8 +goal Set.thy "A <= B <-> (ALL x. x:A --> x:B)";
    13.9  by (fast_tac set_cs 1);
   13.10  qed "subsetXH";
   13.11  
   13.12 @@ -25,18 +25,18 @@
   13.13  val XH_tac = mk_XH_tac Type.thy simp_type_defs [];
   13.14  
   13.15  val EmptyXH = XH_tac "a : {} <-> False";
   13.16 -val SubtypeXH = XH_tac "a : {x:A.P(x)} <-> (a:A & P(a))";
   13.17 +val SubtypeXH = XH_tac "a : {x:A. P(x)} <-> (a:A & P(a))";
   13.18  val UnitXH = XH_tac "a : Unit          <-> a=one";
   13.19  val BoolXH = XH_tac "a : Bool          <-> a=true | a=false";
   13.20 -val PlusXH = XH_tac "a : A+B           <-> (EX x:A.a=inl(x)) | (EX x:B.a=inr(x))";
   13.21 -val PiXH   = XH_tac "a : PROD x:A.B(x) <-> (EX b.a=lam x.b(x) & (ALL x:A.b(x):B(x)))";
   13.22 -val SgXH   = XH_tac "a : SUM x:A.B(x)  <-> (EX x:A.EX y:B(x).a=<x,y>)";
   13.23 +val PlusXH = XH_tac "a : A+B           <-> (EX x:A. a=inl(x)) | (EX x:B. a=inr(x))";
   13.24 +val PiXH   = XH_tac "a : PROD x:A. B(x) <-> (EX b. a=lam x. b(x) & (ALL x:A. b(x):B(x)))";
   13.25 +val SgXH   = XH_tac "a : SUM x:A. B(x)  <-> (EX x:A. EX y:B(x).a=<x,y>)";
   13.26  
   13.27  val XHs = [EmptyXH,SubtypeXH,UnitXH,BoolXH,PlusXH,PiXH,SgXH];
   13.28  
   13.29  val LiftXH = XH_tac "a : [A] <-> (a=bot | a:A)";
   13.30 -val TallXH = XH_tac "a : TALL X.B(X) <-> (ALL X. a:B(X))";
   13.31 -val TexXH  = XH_tac "a : TEX X.B(X) <-> (EX X. a:B(X))";
   13.32 +val TallXH = XH_tac "a : TALL X. B(X) <-> (ALL X. a:B(X))";
   13.33 +val TexXH  = XH_tac "a : TEX X. B(X) <-> (EX X. a:B(X))";
   13.34  
   13.35  val case_rls = XH_to_Es XHs;
   13.36  
   13.37 @@ -49,7 +49,7 @@
   13.38  val oneT   = canT_tac "one : Unit";
   13.39  val trueT  = canT_tac "true : Bool";
   13.40  val falseT = canT_tac "false : Bool";
   13.41 -val lamT   = canT_tac "[| !!x.x:A ==> b(x):B(x) |] ==> lam x.b(x) : Pi(A,B)";
   13.42 +val lamT   = canT_tac "[| !!x. x:A ==> b(x):B(x) |] ==> lam x. b(x) : Pi(A,B)";
   13.43  val pairT  = canT_tac "[| a:A; b:B(a) |] ==> <a,b>:Sigma(A,B)";
   13.44  val inlT   = canT_tac "a:A ==> inl(a) : A+B";
   13.45  val inrT   = canT_tac "b:B ==> inr(b) : A+B";
   13.46 @@ -108,16 +108,16 @@
   13.47  
   13.48  (*** Monotonicity ***)
   13.49  
   13.50 -goal Type.thy "mono (%X.X)";
   13.51 +goal Type.thy "mono (%X. X)";
   13.52  by (REPEAT (ares_tac [monoI] 1));
   13.53  qed "idM";
   13.54  
   13.55 -goal Type.thy "mono(%X.A)";
   13.56 +goal Type.thy "mono(%X. A)";
   13.57  by (REPEAT (ares_tac [monoI,subset_refl] 1));
   13.58  qed "constM";
   13.59  
   13.60  val major::prems = goal Type.thy
   13.61 -    "mono(%X.A(X)) ==> mono(%X.[A(X)])";
   13.62 +    "mono(%X. A(X)) ==> mono(%X.[A(X)])";
   13.63  by (rtac (subsetI RS monoI) 1);
   13.64  by (dtac (LiftXH RS iffD1) 1);
   13.65  by (etac disjE 1);
   13.66 @@ -128,8 +128,8 @@
   13.67  qed "LiftM";
   13.68  
   13.69  val prems = goal Type.thy
   13.70 -    "[| mono(%X.A(X)); !!x X. x:A(X) ==> mono(%X.B(X,x)) |] ==> \
   13.71 -\    mono(%X.Sigma(A(X),B(X)))";
   13.72 +    "[| mono(%X. A(X)); !!x X. x:A(X) ==> mono(%X. B(X,x)) |] ==> \
   13.73 +\    mono(%X. Sigma(A(X),B(X)))";
   13.74  by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   13.75              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   13.76              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   13.77 @@ -137,7 +137,7 @@
   13.78  qed "SgM";
   13.79  
   13.80  val prems = goal Type.thy
   13.81 -    "[| !!x. x:A ==> mono(%X.B(X,x)) |] ==> mono(%X.Pi(A,B(X)))";
   13.82 +    "[| !!x. x:A ==> mono(%X. B(X,x)) |] ==> mono(%X. Pi(A,B(X)))";
   13.83  by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   13.84              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   13.85              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   13.86 @@ -145,7 +145,7 @@
   13.87  qed "PiM";
   13.88  
   13.89  val prems = goal Type.thy
   13.90 -     "[| mono(%X.A(X));  mono(%X.B(X)) |] ==> mono(%X.A(X)+B(X))";
   13.91 +     "[| mono(%X. A(X));  mono(%X. B(X)) |] ==> mono(%X. A(X)+B(X))";
   13.92  by (REPEAT (ares_tac ([subsetI RS monoI] @ canTs) 1 ORELSE
   13.93              eresolve_tac ([bspec,exE,conjE,disjE,bexE] @ case_rls) 1 ORELSE
   13.94              (resolve_tac (prems RL [monoD RS subsetD]) 1 THEN assume_tac 1) ORELSE
   13.95 @@ -156,18 +156,18 @@
   13.96  
   13.97  (*** Conversion Rules for Fixed Points via monotonicity and Tarski ***)
   13.98  
   13.99 -goal Type.thy "mono(%X.Unit+X)";
  13.100 +goal Type.thy "mono(%X. Unit+X)";
  13.101  by (REPEAT (ares_tac [PlusM,constM,idM] 1));
  13.102  qed "NatM";
  13.103  bind_thm("def_NatB", result() RS (Nat_def RS def_lfp_Tarski));
  13.104  
  13.105 -goal Type.thy "mono(%X.(Unit+Sigma(A,%y.X)))";
  13.106 +goal Type.thy "mono(%X.(Unit+Sigma(A,%y. X)))";
  13.107  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
  13.108  qed "ListM";
  13.109  bind_thm("def_ListB", result() RS (List_def RS def_lfp_Tarski));
  13.110  bind_thm("def_ListsB", result() RS (Lists_def RS def_gfp_Tarski));
  13.111  
  13.112 -goal Type.thy "mono(%X.({} + Sigma(A,%y.X)))";
  13.113 +goal Type.thy "mono(%X.({} + Sigma(A,%y. X)))";
  13.114  by (REPEAT (ares_tac [PlusM,SgM,constM,idM] 1));
  13.115  qed "IListsM";
  13.116  bind_thm("def_IListsB", result() RS (ILists_def RS def_gfp_Tarski));
  13.117 @@ -182,10 +182,10 @@
  13.118  
  13.119  val iXH_tac = mk_iXH_tac ind_type_eqs ind_data_defs [];
  13.120  
  13.121 -val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat.a=succ(x)))";
  13.122 -val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A.EX xs:List(A).a=x$xs))";
  13.123 -val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A.EX xs:Lists(A).a=x$xs))";
  13.124 -val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A.EX xs:ILists(A).a=x$xs)";
  13.125 +val NatXH  = iXH_tac "a : Nat <-> (a=zero | (EX x:Nat. a=succ(x)))";
  13.126 +val ListXH = iXH_tac "a : List(A) <-> (a=[] | (EX x:A. EX xs:List(A).a=x$xs))";
  13.127 +val ListsXH = iXH_tac "a : Lists(A) <-> (a=[] | (EX x:A. EX xs:Lists(A).a=x$xs))";
  13.128 +val IListsXH = iXH_tac "a : ILists(A) <-> (EX x:A. EX xs:ILists(A).a=x$xs)";
  13.129  
  13.130  val iXHs = [NatXH,ListXH];
  13.131  val icase_rls = XH_to_Es iXHs;
  13.132 @@ -283,15 +283,15 @@
  13.133  qed "lfp_subset_gfp";
  13.134  
  13.135  val prems = goal Type.thy
  13.136 -    "[| a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
  13.137 +    "[| a:A;  !!x X.[| x:A;  ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \
  13.138  \    t(a) : gfp(B)";
  13.139  by (rtac coinduct 1);
  13.140 -by (res_inst_tac [("P","%x.EX y:A.x=t(y)")] CollectI 1);
  13.141 +by (res_inst_tac [("P","%x. EX y:A. x=t(y)")] CollectI 1);
  13.142  by (ALLGOALS (fast_tac (ccl_cs addSIs prems)));
  13.143  qed "gfpI";
  13.144  
  13.145  val rew::prem::prems = goal Type.thy
  13.146 -    "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A.t(y):X |] ==> t(x) : B(X) |] ==> \
  13.147 +    "[| C==gfp(B);  a:A;  !!x X.[| x:A;  ALL y:A. t(y):X |] ==> t(x) : B(X) |] ==> \
  13.148  \    t(a) : C";
  13.149  by (rewtac rew);
  13.150  by (REPEAT (ares_tac ((prem RS gfpI)::prems) 1));
    14.1 --- a/src/CCL/Type.thy	Fri Oct 10 16:29:41 1997 +0200
    14.2 +++ b/src/CCL/Type.thy	Fri Oct 10 17:10:12 1997 +0200
    14.3 @@ -46,23 +46,23 @@
    14.4  
    14.5  rules
    14.6  
    14.7 -  Subtype_def "{x:A.P(x)} == {x.x:A & P(x)}"
    14.8 -  Unit_def          "Unit == {x.x=one}"
    14.9 -  Bool_def          "Bool == {x.x=true | x=false}"
   14.10 -  Plus_def           "A+B == {x. (EX a:A.x=inl(a)) | (EX b:B.x=inr(b))}"
   14.11 -  Pi_def         "Pi(A,B) == {x.EX b.x=lam x.b(x) & (ALL x:A.b(x):B(x))}"
   14.12 -  Sigma_def   "Sigma(A,B) == {x.EX a:A.EX b:B(a).x=<a,b>}"
   14.13 -  Nat_def            "Nat == lfp(% X.Unit + X)"
   14.14 -  List_def       "List(A) == lfp(% X.Unit + A*X)"
   14.15 +  Subtype_def "{x:A. P(x)} == {x. x:A & P(x)}"
   14.16 +  Unit_def          "Unit == {x. x=one}"
   14.17 +  Bool_def          "Bool == {x. x=true | x=false}"
   14.18 +  Plus_def           "A+B == {x. (EX a:A. x=inl(a)) | (EX b:B. x=inr(b))}"
   14.19 +  Pi_def         "Pi(A,B) == {x. EX b. x=lam x. b(x) & (ALL x:A. b(x):B(x))}"
   14.20 +  Sigma_def   "Sigma(A,B) == {x. EX a:A. EX b:B(a).x=<a,b>}"
   14.21 +  Nat_def            "Nat == lfp(% X. Unit + X)"
   14.22 +  List_def       "List(A) == lfp(% X. Unit + A*X)"
   14.23  
   14.24 -  Lists_def     "Lists(A) == gfp(% X.Unit + A*X)"
   14.25 +  Lists_def     "Lists(A) == gfp(% X. Unit + A*X)"
   14.26    ILists_def   "ILists(A) == gfp(% X.{} + A*X)"
   14.27  
   14.28 -  Tall_def   "TALL X.B(X) == Inter({X.EX Y.X=B(Y)})"
   14.29 -  Tex_def     "TEX X.B(X) == Union({X.EX Y.X=B(Y)})"
   14.30 +  Tall_def   "TALL X. B(X) == Inter({X. EX Y. X=B(Y)})"
   14.31 +  Tex_def     "TEX X. B(X) == Union({X. EX Y. X=B(Y)})"
   14.32    Lift_def           "[A] == A Un {bot}"
   14.33  
   14.34 -  SPLIT_def   "SPLIT(p,B) == Union({A.EX x y.p=<x,y> & A=B(x,y)})"
   14.35 +  SPLIT_def   "SPLIT(p,B) == Union({A. EX x y. p=<x,y> & A=B(x,y)})"
   14.36  
   14.37  end
   14.38  
    15.1 --- a/src/CCL/Wfd.ML	Fri Oct 10 16:29:41 1997 +0200
    15.2 +++ b/src/CCL/Wfd.ML	Fri Oct 10 17:10:12 1997 +0200
    15.3 @@ -25,7 +25,7 @@
    15.4  val [p1,p2,p3] = goal Wfd.thy
    15.5      "[| !!x y.<x,y> : R ==> Q(x); \
    15.6  \       ALL x. (ALL y. <y,x> : R --> y : P) --> x : P; \
    15.7 -\       !!x.Q(x) ==> x:P |] ==> a:P";
    15.8 +\       !!x. Q(x) ==> x:P |] ==> a:P";
    15.9  by (rtac (p2 RS  spec  RS mp) 1);
   15.10  by (fast_tac (set_cs addSIs [p1 RS p3]) 1);
   15.11  qed "wfd_strengthen_lemma";
   15.12 @@ -64,7 +64,7 @@
   15.13  (*** Lexicographic Ordering ***)
   15.14  
   15.15  goalw Wfd.thy [lex_def] 
   15.16 - "p : ra**rb <-> (EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
   15.17 + "p : ra**rb <-> (EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb))";
   15.18  by (fast_tac ccl_cs 1);
   15.19  qed "lexXH";
   15.20  
   15.21 @@ -98,7 +98,7 @@
   15.22   "[| Wfd(R); Wfd(S) |] ==> Wfd(R**S)";
   15.23  by (rewtac Wfd_def);
   15.24  by (safe_tac ccl_cs);
   15.25 -by (wfd_strengthen_tac "%x.EX a b.x=<a,b>" 1);
   15.26 +by (wfd_strengthen_tac "%x. EX a b. x=<a,b>" 1);
   15.27  by (fast_tac (term_cs addSEs [lex_pair]) 1);
   15.28  by (subgoal_tac "ALL a b.<a,b>:P" 1);
   15.29  by (fast_tac ccl_cs 1);
   15.30 @@ -130,7 +130,7 @@
   15.31   "Wfd(r) ==> Wfd(wmap(f,r))";
   15.32  by (rewtac Wfd_def);
   15.33  by (safe_tac ccl_cs);
   15.34 -by (subgoal_tac "ALL b.ALL a.f(a)=b-->a:P" 1);
   15.35 +by (subgoal_tac "ALL b. ALL a. f(a)=b-->a:P" 1);
   15.36  by (fast_tac ccl_cs 1);
   15.37  by (rtac (wf RS wfd_induct RS allI) 1);
   15.38  by (safe_tac ccl_cs);
   15.39 @@ -175,11 +175,11 @@
   15.40  by (rtac Empty_wf 1);
   15.41  qed "wf_wf";
   15.42  
   15.43 -goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat.p=<x,succ(x)>)";
   15.44 +goalw Wfd.thy [NatPR_def]  "p : NatPR <-> (EX x:Nat. p=<x,succ(x)>)";
   15.45  by (fast_tac set_cs 1);
   15.46  qed "NatPRXH";
   15.47  
   15.48 -goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A.EX t:List(A).p=<t,h$t>)";
   15.49 +goalw Wfd.thy [ListPR_def]  "p : ListPR(A) <-> (EX h:A. EX t:List(A).p=<t,h$t>)";
   15.50  by (fast_tac set_cs 1);
   15.51  qed "ListPRXH";
   15.52  
   15.53 @@ -188,7 +188,7 @@
   15.54  
   15.55  goalw Wfd.thy [Wfd_def]  "Wfd(NatPR)";
   15.56  by (safe_tac set_cs);
   15.57 -by (wfd_strengthen_tac "%x.x:Nat" 1);
   15.58 +by (wfd_strengthen_tac "%x. x:Nat" 1);
   15.59  by (fast_tac (type_cs addSEs [XH_to_E NatPRXH]) 1);
   15.60  by (etac Nat_ind 1);
   15.61  by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E NatPRXH])));
   15.62 @@ -196,7 +196,7 @@
   15.63  
   15.64  goalw Wfd.thy [Wfd_def]  "Wfd(ListPR(A))";
   15.65  by (safe_tac set_cs);
   15.66 -by (wfd_strengthen_tac "%x.x:List(A)" 1);
   15.67 +by (wfd_strengthen_tac "%x. x:List(A)" 1);
   15.68  by (fast_tac (type_cs addSEs [XH_to_E ListPRXH]) 1);
   15.69  by (etac List_ind 1);
   15.70  by (ALLGOALS (fast_tac (type_cs addEs [XH_to_E ListPRXH])));
    16.1 --- a/src/CCL/Wfd.thy	Fri Oct 10 16:29:41 1997 +0200
    16.2 +++ b/src/CCL/Wfd.thy	Fri Oct 10 17:10:12 1997 +0200
    16.3 @@ -21,14 +21,14 @@
    16.4  rules
    16.5  
    16.6    Wfd_def
    16.7 -  "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a.a:P)"
    16.8 +  "Wfd(R) == ALL P.(ALL x.(ALL y.<y,x> : R --> y:P) --> x:P) --> (ALL a. a:P)"
    16.9  
   16.10 -  wf_def         "wf(R) == {x.x:R & Wfd(R)}"
   16.11 +  wf_def         "wf(R) == {x. x:R & Wfd(R)}"
   16.12  
   16.13    wmap_def       "wmap(f,R) == {p. EX x y. p=<x,y>  &  <f(x),f(y)> : R}"
   16.14    lex_def
   16.15 -  "ra**rb == {p. EX a a' b b'.p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
   16.16 +  "ra**rb == {p. EX a a' b b'. p = <<a,b>,<a',b'>> & (<a,a'> : ra | (a=a' & <b,b'> : rb))}"
   16.17  
   16.18 -  NatPR_def      "NatPR == {p.EX x:Nat. p=<x,succ(x)>}"
   16.19 -  ListPR_def     "ListPR(A) == {p.EX h:A.EX t:List(A). p=<t,h$t>}"
   16.20 +  NatPR_def      "NatPR == {p. EX x:Nat. p=<x,succ(x)>}"
   16.21 +  ListPR_def     "ListPR(A) == {p. EX h:A. EX t:List(A). p=<t,h$t>}"
   16.22  end
    17.1 --- a/src/CCL/coinduction.ML	Fri Oct 10 16:29:41 1997 +0200
    17.2 +++ b/src/CCL/coinduction.ML	Fri Oct 10 17:10:12 1997 +0200
    17.3 @@ -48,7 +48,7 @@
    17.4        ["<true,true> : POgen(R)",
    17.5         "<false,false> : POgen(R)",
    17.6         "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : POgen(R)",
    17.7 -       "[|!!x. <b(x),b'(x)> : R |] ==><lam x.b(x),lam x.b'(x)> : POgen(R)",
    17.8 +       "[|!!x. <b(x),b'(x)> : R |] ==><lam x. b(x),lam x. b'(x)> : POgen(R)",
    17.9         "<one,one> : POgen(R)",
   17.10         "<a,a'> : lfp(%x. POgen(x) Un R Un PO) ==> \
   17.11  \                         <inl(a),inl(a')> : POgen(lfp(%x. POgen(x) Un R Un PO))",
   17.12 @@ -78,7 +78,7 @@
   17.13  ["<true,true> : EQgen(R)",
   17.14   "<false,false> : EQgen(R)",
   17.15   "[| <a,a'> : R;  <b,b'> : R |] ==> <<a,b>,<a',b'>> : EQgen(R)",
   17.16 - "[|!!x. <b(x),b'(x)> : R |] ==> <lam x.b(x),lam x.b'(x)> : EQgen(R)",
   17.17 + "[|!!x. <b(x),b'(x)> : R |] ==> <lam x. b(x),lam x. b'(x)> : EQgen(R)",
   17.18   "<one,one> : EQgen(R)",
   17.19   "<a,a'> : lfp(%x. EQgen(x) Un R Un EQ) ==> \
   17.20  \                   <inl(a),inl(a')> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))",
    18.1 --- a/src/CCL/equalities.ML	Fri Oct 10 16:29:41 1997 +0200
    18.2 +++ b/src/CCL/equalities.ML	Fri Oct 10 17:10:12 1997 +0200
    18.3 @@ -64,11 +64,11 @@
    18.4  
    18.5  (** Simple properties of Compl -- complement of a set **)
    18.6  
    18.7 -goal Set.thy "A Int Compl(A) = {x.False}";
    18.8 +goal Set.thy "A Int Compl(A) = {x. False}";
    18.9  by (fast_tac eq_cs 1);
   18.10  qed "Compl_disjoint";
   18.11  
   18.12 -goal Set.thy "A Un Compl(A) = {x.True}";
   18.13 +goal Set.thy "A Un Compl(A) = {x. True}";
   18.14  by (fast_tac eq_cs 1);
   18.15  qed "Compl_partition";
   18.16  
   18.17 @@ -106,7 +106,7 @@
   18.18  qed "Union_Un_distrib";
   18.19  
   18.20  val prems = goal Set.thy
   18.21 -   "(Union(C) Int A = {x.False}) <-> (ALL B:C. B Int A = {x.False})";
   18.22 +   "(Union(C) Int A = {x. False}) <-> (ALL B:C. B Int A = {x. False})";
   18.23  by (fast_tac (eq_cs addSEs [equalityE]) 1);
   18.24  qed "Union_disjoint";
   18.25  
    19.1 --- a/src/CCL/eval.ML	Fri Oct 10 16:29:41 1997 +0200
    19.2 +++ b/src/CCL/eval.ML	Fri Oct 10 17:10:12 1997 +0200
    19.3 @@ -14,7 +14,7 @@
    19.4  fun ceval_tac rls = DEPTH_SOLVE_1 (resolve_tac (!EVal_rls@rls) 1);
    19.5  
    19.6  val prems = goalw thy [apply_def]
    19.7 -   "[| f ---> lam x.b(x);  b(a) ---> c |] ==> f ` a ---> c";
    19.8 +   "[| f ---> lam x. b(x);  b(a) ---> c |] ==> f ` a ---> c";
    19.9  by (ceval_tac prems);
   19.10  qed "applyV";
   19.11  
   19.12 @@ -35,7 +35,7 @@
   19.13  qed "fixV";
   19.14  
   19.15  val prems = goalw thy [letrec_def]
   19.16 -    "h(t,%y.letrec g x be h(x,g) in g(y)) ---> c ==> \
   19.17 +    "h(t,%y. letrec g x be h(x,g) in g(y)) ---> c ==> \
   19.18  \                  letrec g x be h(x,g) in g(t) ---> c";
   19.19  by (REPEAT (resolve_tac (prems @ [fixV,applyV,lamV]) 1));
   19.20  qed "letrecV";
   19.21 @@ -69,19 +69,19 @@
   19.22  (* Factorial *)
   19.23  
   19.24  val prems = goal thy
   19.25 -    "letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
   19.26 +    "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \
   19.27  \              in f(succ(succ(zero))) ---> ?a";
   19.28  by (ceval_tac []);
   19.29  
   19.30  val prems = goal thy
   19.31 -    "letrec f n be ncase(n,succ(zero),%x.nrec(n,zero,%y g.nrec(f(x),g,%z h.succ(h)))) \
   19.32 +    "letrec f n be ncase(n,succ(zero),%x. nrec(n,zero,%y g. nrec(f(x),g,%z h. succ(h)))) \
   19.33  \              in f(succ(succ(succ(zero)))) ---> ?a";
   19.34  by (ceval_tac []);
   19.35  
   19.36  (* Less Than Or Equal *)
   19.37  
   19.38  fun isle x y = prove_goal thy 
   19.39 -    ("letrec f p be split(p,%m n.ncase(m,true,%x.ncase(n,false,%y.f(<x,y>)))) \
   19.40 +    ("letrec f p be split(p,%m n. ncase(m,true,%x. ncase(n,false,%y. f(<x,y>)))) \
   19.41  \              in f(<"^x^","^y^">) ---> ?a")
   19.42      (fn prems => [ceval_tac []]);
   19.43  
   19.44 @@ -93,12 +93,12 @@
   19.45  (* Reverse *)
   19.46  
   19.47  val prems = goal thy
   19.48 -    "letrec id l be lcase(l,[],%x xs.x$id(xs)) \
   19.49 +    "letrec id l be lcase(l,[],%x xs. x$id(xs)) \
   19.50  \              in id(zero$succ(zero)$[]) ---> ?a";
   19.51  by (ceval_tac []);
   19.52  
   19.53  val prems = goal thy
   19.54 -    "letrec rev l be lcase(l,[],%x xs.lrec(rev(xs),x$[],%y ys g.y$g)) \
   19.55 -\              in rev(zero$succ(zero)$(succ((lam x.x)`succ(zero)))$([])) ---> ?a";
   19.56 +    "letrec rev l be lcase(l,[],%x xs. lrec(rev(xs),x$[],%y ys g. y$g)) \
   19.57 +\              in rev(zero$succ(zero)$(succ((lam x. x)`succ(zero)))$([])) ---> ?a";
   19.58  by (ceval_tac []);
   19.59  
    20.1 --- a/src/CCL/ex/Flag.thy	Fri Oct 10 16:29:41 1997 +0200
    20.2 +++ b/src/CCL/ex/Flag.thy	Fri Oct 10 17:10:12 1997 +0200
    20.3 @@ -24,11 +24,11 @@
    20.4    white_def    "white == inr(inl(one))"
    20.5    blue_def     "blue == inr(inr(one))"
    20.6  
    20.7 -  ccase_def   "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"
    20.8 +  ccase_def   "ccase(c,r,w,b) == when(c,%x. r,%wb. when(wb,%x. w,%x. b))"
    20.9  
   20.10 -  flag_def    "flag == lam l.letrec 
   20.11 +  flag_def    "flag == lam l. letrec 
   20.12        flagx l be lcase(l,<[],<[],[]>>, 
   20.13 -                       %h t. split(flagx(t),%lr p.split(p,%lw lb. 
   20.14 +                       %h t. split(flagx(t),%lr p. split(p,%lw lb. 
   20.15                              ccase(h, <red$lr,<lw,lb>>, 
   20.16                                       <lr,<white$lw,lb>>, 
   20.17                                       <lr,<lw,blue$lb>>)))) 
    21.1 --- a/src/CCL/ex/List.ML	Fri Oct 10 16:29:41 1997 +0200
    21.2 +++ b/src/CCL/ex/List.ML	Fri Oct 10 17:10:12 1997 +0200
    21.3 @@ -14,7 +14,7 @@
    21.4  (****)
    21.5  
    21.6  val listBs = map (fn s=>prove_goalw List.thy list_defs s (fn _ => [simp_tac term_ss 1]))
    21.7 -     ["(f o g) = (%a.f(g(a)))",
    21.8 +     ["(f o g) = (%a. f(g(a)))",
    21.9        "(f o g)(a) = f(g(a))",
   21.10        "map(f,[]) = []",
   21.11        "map(f,x$xs) = f(x)$map(f,xs)",
   21.12 @@ -44,7 +44,7 @@
   21.13  (***)
   21.14  
   21.15  val prems = goalw List.thy [map_def]
   21.16 -  "[| !!x.x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)";
   21.17 +  "[| !!x. x:A==>f(x):B;  l : List(A) |] ==> map(f,l) : List(B)";
   21.18  by (typechk_tac prems 1);
   21.19  qed "mapT";
   21.20  
    22.1 --- a/src/CCL/ex/List.thy	Fri Oct 10 16:29:41 1997 +0200
    22.2 +++ b/src/CCL/ex/List.thy	Fri Oct 10 17:10:12 1997 +0200
    22.3 @@ -22,15 +22,15 @@
    22.4  
    22.5  rules 
    22.6  
    22.7 -  map_def     "map(f,l)   == lrec(l,[],%x xs g.f(x)$g)"
    22.8 -  comp_def    "f o g == (%x.f(g(x)))"
    22.9 -  append_def  "l @ m == lrec(l,m,%x xs g.x$g)"
   22.10 -  mem_def     "a mem l == lrec(l,false,%h t g.if eq(a,h) then true else g)"
   22.11 -  filter_def  "filter(f,l) == lrec(l,[],%x xs g.if f`x then x$g else g)"
   22.12 -  flat_def    "flat(l) == lrec(l,[],%h t g.h @ g)"
   22.13 +  map_def     "map(f,l)   == lrec(l,[],%x xs g. f(x)$g)"
   22.14 +  comp_def    "f o g == (%x. f(g(x)))"
   22.15 +  append_def  "l @ m == lrec(l,m,%x xs g. x$g)"
   22.16 +  mem_def     "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
   22.17 +  filter_def  "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
   22.18 +  flat_def    "flat(l) == lrec(l,[],%h t g. h @ g)"
   22.19  
   22.20 -  insert_def  "insert(f,a,l) == lrec(l,a$[],%h t g.if f`a`h then a$h$t else h$g)"
   22.21 -  isort_def   "isort(f) == lam l.lrec(l,[],%h t g.insert(f,h,g))"
   22.22 +  insert_def  "insert(f,a,l) == lrec(l,a$[],%h t g. if f`a`h then a$h$t else h$g)"
   22.23 +  isort_def   "isort(f) == lam l. lrec(l,[],%h t g. insert(f,h,g))"
   22.24  
   22.25    partition_def 
   22.26    "partition(f,l) == letrec part l a b be lcase(l,<a,b>,%x xs.
   22.27 @@ -38,7 +38,7 @@
   22.28                      in part(l,[],[])"
   22.29    qsort_def   "qsort(f) == lam l. letrec qsortx l be lcase(l,[],%h t. 
   22.30                                     let p be partition(f`h,t) 
   22.31 -                                   in split(p,%x y.qsortx(x) @ h$qsortx(y))) 
   22.32 +                                   in split(p,%x y. qsortx(x) @ h$qsortx(y))) 
   22.33                            in qsortx(l)"
   22.34  
   22.35  end
    23.1 --- a/src/CCL/ex/Nat.thy	Fri Oct 10 16:29:41 1997 +0200
    23.2 +++ b/src/CCL/ex/Nat.thy	Fri Oct 10 17:10:12 1997 +0200
    23.3 @@ -19,11 +19,11 @@
    23.4  
    23.5    not_def     "not(b) == if b then false else true"
    23.6  
    23.7 -  add_def     "a #+ b == nrec(a,b,%x g.succ(g))"
    23.8 -  mult_def    "a #* b == nrec(a,zero,%x g.b #+ g)"
    23.9 -  sub_def     "a #- b == letrec sub x y be ncase(y,x,%yy.ncase(x,zero,%xx.sub(xx,yy))) 
   23.10 +  add_def     "a #+ b == nrec(a,b,%x g. succ(g))"
   23.11 +  mult_def    "a #* b == nrec(a,zero,%x g. b #+ g)"
   23.12 +  sub_def     "a #- b == letrec sub x y be ncase(y,x,%yy. ncase(x,zero,%xx. sub(xx,yy))) 
   23.13                          in sub(a,b)"
   23.14 -  le_def     "a #<= b == letrec le x y be ncase(x,true,%xx.ncase(y,false,%yy.le(xx,yy))) 
   23.15 +  le_def     "a #<= b == letrec le x y be ncase(x,true,%xx. ncase(y,false,%yy. le(xx,yy))) 
   23.16                          in le(a,b)"
   23.17    lt_def     "a #< b == not(b #<= a)"
   23.18  
   23.19 @@ -31,7 +31,7 @@
   23.20                         in div(a,b)"
   23.21    ack_def    
   23.22    "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x. 
   23.23 -                          ncase(m,ack(x,succ(zero)),%y.ack(x,ack(succ(x),y))))
   23.24 +                          ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
   23.25                      in ack(a,b)"
   23.26  
   23.27  end
    24.1 --- a/src/CCL/ex/Stream.ML	Fri Oct 10 16:29:41 1997 +0200
    24.2 +++ b/src/CCL/ex/Stream.ML	Fri Oct 10 17:10:12 1997 +0200
    24.3 @@ -16,7 +16,7 @@
    24.4  
    24.5  val prems = goal Stream.thy "l:Lists(A) ==> map(f o g,l) = map(f,map(g,l))";
    24.6  by (eq_coinduct3_tac 
    24.7 -       "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}"  1);
    24.8 +       "{p. EX x y. p=<x,y> & (EX l:Lists(A).x=map(f o g,l) & y=map(f,map(g,l)))}"  1);
    24.9  by (fast_tac (ccl_cs addSIs prems) 1);
   24.10  by (safe_tac type_cs);
   24.11  by (etac (XH_to_E ListsXH) 1);
   24.12 @@ -27,9 +27,9 @@
   24.13  
   24.14  (*** Mapping the identity function leaves a list unchanged ***)
   24.15  
   24.16 -val prems = goal Stream.thy "l:Lists(A) ==> map(%x.x,l) = l";
   24.17 +val prems = goal Stream.thy "l:Lists(A) ==> map(%x. x,l) = l";
   24.18  by (eq_coinduct3_tac 
   24.19 -       "{p. EX x y.p=<x,y> & (EX l:Lists(A).x=map(%x.x,l) & y=l)}"  1);
   24.20 +       "{p. EX x y. p=<x,y> & (EX l:Lists(A).x=map(%x. x,l) & y=l)}"  1);
   24.21  by (fast_tac (ccl_cs addSIs prems) 1);
   24.22  by (safe_tac type_cs);
   24.23  by (etac (XH_to_E ListsXH) 1);
   24.24 @@ -41,7 +41,7 @@
   24.25  
   24.26  val prems = goal Stream.thy 
   24.27          "[| l:Lists(A); m:Lists(A) |] ==> map(f,l@m) = map(f,l) @ map(f,m)";
   24.28 -by (eq_coinduct3_tac "{p. EX x y.p=<x,y> & (EX l:Lists(A).EX m:Lists(A). \
   24.29 +by (eq_coinduct3_tac "{p. EX x y. p=<x,y> & (EX l:Lists(A).EX m:Lists(A). \
   24.30  \                                           x=map(f,l@m) & y=map(f,l) @ map(f,m))}"  1);
   24.31  by (fast_tac (ccl_cs addSIs prems) 1);
   24.32  by (safe_tac type_cs);
   24.33 @@ -57,7 +57,7 @@
   24.34  val prems = goal Stream.thy 
   24.35          "[| k:Lists(A); l:Lists(A); m:Lists(A) |] ==> k @ l @ m = (k @ l) @ m";
   24.36  by (eq_coinduct3_tac 
   24.37 -    "{p. EX x y.p=<x,y> & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \
   24.38 +    "{p. EX x y. p=<x,y> & (EX k:Lists(A).EX l:Lists(A).EX m:Lists(A). \
   24.39  \                          x=k @ l @ m & y=(k @ l) @ m)}"  1);
   24.40  by (fast_tac (ccl_cs addSIs prems) 1);
   24.41  by (safe_tac type_cs);
   24.42 @@ -71,7 +71,7 @@
   24.43  
   24.44  val prems = goal Stream.thy "l:ILists(A) ==> l @ m = l";
   24.45  by (eq_coinduct3_tac
   24.46 -    "{p. EX x y.p=<x,y> & (EX l:ILists(A).EX m.x=l@m & y=l)}" 1);
   24.47 +    "{p. EX x y. p=<x,y> & (EX l:ILists(A).EX m. x=l@m & y=l)}" 1);
   24.48  by (fast_tac (ccl_cs addSIs prems) 1);
   24.49  by (safe_tac set_cs);
   24.50  by (etac (XH_to_E IListsXH) 1);
   24.51 @@ -103,7 +103,7 @@
   24.52  
   24.53  goal Stream.thy "iter1(f,a) = iter2(f,a)";
   24.54  by (eq_coinduct3_tac 
   24.55 -    "{p. EX x y.p=<x,y> & (EX n:Nat.x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
   24.56 +    "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1(f,f^n`a) & y=map(f)^n`iter2(f,a))}"
   24.57      1);
   24.58  by (fast_tac (type_cs addSIs [napplyBzero RS sym,
   24.59                                napplyBzero RS sym RS arg_cong]) 1);
    25.1 --- a/src/CCL/genrec.ML	Fri Oct 10 16:29:41 1997 +0200
    25.2 +++ b/src/CCL/genrec.ML	Fri Oct 10 17:10:12 1997 +0200
    25.3 @@ -30,7 +30,7 @@
    25.4  val prems = goalw Wfd.thy [letrec2_def]
    25.5      "[| a : A;  b : B;  \
    25.6  \     !!p q g.[| p:A; q:B; \
    25.7 -\             ALL x:A.ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
    25.8 +\             ALL x:A. ALL y:{y: B. <<x,y>,<p,q>>:wf(R)}. g(x,y) : D(x,y) |] ==>\
    25.9  \               h(p,q,g) : D(p,q) |] ==> \
   25.10  \    letrec g x y be h(x,y,g) in g(a,b) : D(a,b)";
   25.11  by (rtac (SPLITB RS subst) 1);
   25.12 @@ -42,14 +42,14 @@
   25.13              eresolve_tac [bspec,SubtypeE,sym RS subst] 1));
   25.14  qed "letrec2T";
   25.15  
   25.16 -goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs.SPLIT(xs,%y z.B(x,y,z))) = B(a,b,c)";
   25.17 +goal Wfd.thy "SPLIT(<a,<b,c>>,%x xs. SPLIT(xs,%y z. B(x,y,z))) = B(a,b,c)";
   25.18  by (simp_tac (ccl_ss addsimps [SPLITB]) 1);
   25.19  qed "lemma";
   25.20  
   25.21  val prems = goalw Wfd.thy [letrec3_def]
   25.22      "[| a : A;  b : B;  c : C;  \
   25.23  \    !!p q r g.[| p:A; q:B; r:C; \
   25.24 -\      ALL x:A.ALL y:B.ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
   25.25 +\      ALL x:A. ALL y:B. ALL z:{z:C. <<x,<y,z>>,<p,<q,r>>> : wf(R)}. \
   25.26  \                                                       g(x,y,z) : D(x,y,z) |] ==>\
   25.27  \               h(p,q,r,g) : D(p,q,r) |] ==> \
   25.28  \    letrec g x y z be h(x,y,z,g) in g(a,b,c) : D(a,b,c)";
   25.29 @@ -75,14 +75,14 @@
   25.30  qed "rcallT";
   25.31  
   25.32  val major::prems = goal Wfd.thy
   25.33 -    "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
   25.34 +    "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
   25.35  \       g(a,b) : D(a,b) ==> g(a,b) : E;  a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
   25.36  \   g(a,b) : E";
   25.37  by (REPEAT (ares_tac ([SubtypeI,major RS bspec RS bspec,major]@prems) 1));
   25.38  qed "rcall2T";
   25.39  
   25.40  val major::prems = goal Wfd.thy
   25.41 -    "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
   25.42 +    "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}. g(x,y,z):D(x,y,z); \
   25.43  \       g(a,b,c) : D(a,b,c) ==> g(a,b,c) : E;  \
   25.44  \       a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
   25.45  \   g(a,b,c) : E";
   25.46 @@ -116,7 +116,7 @@
   25.47  qed "hyprcallT";
   25.48  
   25.49  val prems = goal Wfd.thy
   25.50 -    "[| g(a,b) = c; ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
   25.51 +    "[| g(a,b) = c; ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); \
   25.52  \       [| c=g(a,b);  g(a,b) : D(a,b) |] ==> P; \
   25.53  \       a:A;  b:B;  <<a,b>,<p,q>>:wf(R) |] ==> \
   25.54  \   P";
   25.55 @@ -128,7 +128,7 @@
   25.56  
   25.57  val prems = goal Wfd.thy
   25.58    "[| g(a,b,c) = d; \
   25.59 -\     ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
   25.60 +\     ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
   25.61  \   [| d=g(a,b,c);  g(a,b,c) : D(a,b,c) |] ==> P; \
   25.62  \   a:A;  b:B;  c:C;  <<a,<b,c>>,<p,<q,r>>> : wf(R) |] ==> \
   25.63  \   P";
   25.64 @@ -149,13 +149,13 @@
   25.65  qed "rmIH1";
   25.66  
   25.67  val prems = goal Wfd.thy
   25.68 -    "[| ALL x:A.ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
   25.69 +    "[| ALL x:A. ALL y:{y:B.<<x,y>,<p,q>>:wf(R)}.g(x,y):D(x,y); P |] ==> \
   25.70  \    P";
   25.71  by (REPEAT (ares_tac prems 1));
   25.72  qed "rmIH2";
   25.73  
   25.74  val prems = goal Wfd.thy
   25.75 - "[| ALL x:A.ALL y:B.ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
   25.76 + "[| ALL x:A. ALL y:B. ALL z:{z:C.<<x,<y,z>>,<p,<q,r>>>:wf(R)}.g(x,y,z):D(x,y,z); \
   25.77  \    P |] ==> \
   25.78  \    P";
   25.79  by (REPEAT (ares_tac prems 1));
    26.1 --- a/src/CCL/subset.ML	Fri Oct 10 16:29:41 1997 +0200
    26.2 +++ b/src/CCL/subset.ML	Fri Oct 10 17:10:12 1997 +0200
    26.3 @@ -115,7 +115,7 @@
    26.4     "(a : Compl(B)) <->  (~a:B)",
    26.5     "(a : {b})      <->  (a=b)",
    26.6     "(a : {})       <->   False",
    26.7 -   "(a : {x.P(x)}) <->  P(a)" ]);
    26.8 +   "(a : {x. P(x)}) <->  P(a)" ]);
    26.9  
   26.10  val set_congs = [ball_cong, bex_cong, INT_cong, UN_cong];
   26.11  
    27.1 --- a/src/CCL/typecheck.ML	Fri Oct 10 16:29:41 1997 +0200
    27.2 +++ b/src/CCL/typecheck.ML	Fri Oct 10 17:10:12 1997 +0200
    27.3 @@ -35,9 +35,9 @@
    27.4             fun solve s = prove_goal Type.thy s (fn prems => [tac prems])
    27.5         in map solve
    27.6             ["a : {x:A. b:{y:B(a).P(<x,y>)}} ==> <a,b> : {x:Sigma(A,B).P(x)}",
    27.7 -            "a : {x:A.P(inl(x))} ==> inl(a) : {x:A+B.P(x)}",
    27.8 -            "b : {x:B.P(inr(x))} ==> inr(b) : {x:A+B.P(x)}",
    27.9 -            "a : {x:Nat.P(succ(x))} ==> succ(a) : {x:Nat.P(x)}",
   27.10 +            "a : {x:A. P(inl(x))} ==> inl(a) : {x:A+B. P(x)}",
   27.11 +            "b : {x:B. P(inr(x))} ==> inr(b) : {x:A+B. P(x)}",
   27.12 +            "a : {x:Nat. P(succ(x))} ==> succ(a) : {x:Nat. P(x)}",
   27.13              "h : {x:A. t : {y:List(A).P(x$y)}} ==> h$t : {x:List(A).P(x)}"
   27.14          ] end;
   27.15  
   27.16 @@ -54,12 +54,12 @@
   27.17  qed "applyT2";
   27.18  
   27.19  val prems = goal Type.thy 
   27.20 -    "[| a:A;  a:A ==> P(a) |] ==> a : {x:A.P(x)}";
   27.21 +    "[| a:A;  a:A ==> P(a) |] ==> a : {x:A. P(x)}";
   27.22  by (fast_tac (type_cs addSIs prems) 1);
   27.23  qed "rcall_lemma1";
   27.24  
   27.25  val prems = goal Type.thy 
   27.26 -    "[| a:{x:A.Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A.P(x)}";
   27.27 +    "[| a:{x:A. Q(x)};  [| a:A; Q(a) |] ==> P(a) |] ==> a : {x:A. P(x)}";
   27.28  by (cut_facts_tac prems 1);
   27.29  by (fast_tac (type_cs addSIs prems) 1);
   27.30  qed "rcall_lemma2";
    28.1 --- a/src/CTT/Arith.ML	Fri Oct 10 16:29:41 1997 +0200
    28.2 +++ b/src/CTT/Arith.ML	Fri Oct 10 17:10:12 1997 +0200
    28.3 @@ -385,7 +385,7 @@
    28.4    [ (rew_tac(absdiff_typing::prems)) ]);
    28.5  
    28.6  qed_goalw "modC_succ" Arith.thy [mod_def] 
    28.7 -"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y.succ(a mod b)) : N"
    28.8 +"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
    28.9   (fn prems=>
   28.10    [ (rew_tac(absdiff_typing::prems)) ]);
   28.11  
   28.12 @@ -429,7 +429,7 @@
   28.13  
   28.14  (*for case analysis on whether a number is 0 or a successor*)
   28.15  qed_goal "iszero_decidable" Arith.thy
   28.16 -    "a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \
   28.17 +    "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \
   28.18  \                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
   28.19   (fn prems=>
   28.20    [ (NE_tac "a" 1),
    29.1 --- a/src/CTT/Arith.thy	Fri Oct 10 16:29:41 1997 +0200
    29.2 +++ b/src/CTT/Arith.thy	Fri Oct 10 17:10:12 1997 +0200
    29.3 @@ -15,10 +15,10 @@
    29.4         "#*",div,mod     :: "[i,i]=>i"   (infixr 70)
    29.5  
    29.6  rules
    29.7 -  add_def     "a#+b == rec(a, b, %u v.succ(v))"  
    29.8 -  diff_def    "a-b == rec(b, a, %u v.rec(v, 0, %x y.x))"  
    29.9 +  add_def     "a#+b == rec(a, b, %u v. succ(v))"  
   29.10 +  diff_def    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"  
   29.11    absdiff_def "a|-|b == (a-b) #+ (b-a)"  
   29.12    mult_def    "a#*b == rec(a, 0, %u v. b #+ v)"  
   29.13 -  mod_def     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y.succ(v)))"
   29.14 -  div_def     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y.v))"
   29.15 +  mod_def     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
   29.16 +  div_def     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
   29.17  end
    30.1 --- a/src/CTT/Bool.thy	Fri Oct 10 16:29:41 1997 +0200
    30.2 +++ b/src/CTT/Bool.thy	Fri Oct 10 17:10:12 1997 +0200
    30.3 @@ -15,5 +15,5 @@
    30.4    Bool_def      "Bool == T+T"
    30.5    true_def      "true == inl(tt)"
    30.6    false_def     "false == inr(tt)"
    30.7 -  cond_def      "cond(a,b,c) == when(a, %u.b, %u.c)"
    30.8 +  cond_def      "cond(a,b,c) == when(a, %u. b, %u. c)"
    30.9  end
    31.1 --- a/src/CTT/CTT.ML	Fri Oct 10 16:29:41 1997 +0200
    31.2 +++ b/src/CTT/CTT.ML	Fri Oct 10 17:10:12 1997 +0200
    31.3 @@ -109,7 +109,7 @@
    31.4  
    31.5  (*Simplify the parameter of a unary type operator.*)
    31.6  qed_goal "subst_eqtyparg" CTT.thy
    31.7 -    "a=c : A ==> (!!z.z:A ==> B(z) type) ==> B(a)=B(c)"
    31.8 +    "a=c : A ==> (!!z. z:A ==> B(z) type) ==> B(a)=B(c)"
    31.9   (fn prems=>
   31.10    [ (rtac subst_typeL 1),
   31.11      (rtac refl_type 2),
    32.1 --- a/src/CTT/CTT.thy	Fri Oct 10 16:29:41 1997 +0200
    32.2 +++ b/src/CTT/CTT.thy	Fri Oct 10 17:10:12 1997 +0200
    32.3 @@ -113,21 +113,21 @@
    32.4  
    32.5    NE
    32.6     "[| p: N;  a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
    32.7 -   ==> rec(p, a, %u v.b(u,v)) : C(p)"
    32.8 +   ==> rec(p, a, %u v. b(u,v)) : C(p)"
    32.9  
   32.10    NEL
   32.11     "[| p = q : N;  a = c : C(0);  
   32.12        !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u)) |] 
   32.13 -   ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)"
   32.14 +   ==> rec(p, a, %u v. b(u,v)) = rec(q,c,d) : C(p)"
   32.15  
   32.16    NC0
   32.17     "[| a: C(0);  !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] 
   32.18 -   ==> rec(0, a, %u v.b(u,v)) = a : C(0)"
   32.19 +   ==> rec(0, a, %u v. b(u,v)) = a : C(0)"
   32.20  
   32.21    NC_succ
   32.22     "[| p: N;  a: C(0);  
   32.23         !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u)) |] ==>  
   32.24 -   rec(succ(p), a, %u v.b(u,v)) = b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))"
   32.25 +   rec(succ(p), a, %u v. b(u,v)) = b(p, rec(p, a, %u v. b(u,v))) : C(succ(p))"
   32.26  
   32.27    (*The fourth Peano axiom.  See page 91 of Martin-Lof's book*)
   32.28    zero_ne_succ
   32.29 @@ -136,54 +136,54 @@
   32.30  
   32.31    (*The Product of a family of types*)
   32.32  
   32.33 -  ProdF  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type"
   32.34 +  ProdF  "[| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type"
   32.35  
   32.36    ProdFL
   32.37     "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> 
   32.38 -   PROD x:A.B(x) = PROD x:C.D(x)"
   32.39 +   PROD x:A. B(x) = PROD x:C. D(x)"
   32.40  
   32.41    ProdI
   32.42 -   "[| A type;  !!x. x:A ==> b(x):B(x)|] ==> lam x.b(x) : PROD x:A.B(x)"
   32.43 +   "[| A type;  !!x. x:A ==> b(x):B(x)|] ==> lam x. b(x) : PROD x:A. B(x)"
   32.44  
   32.45    ProdIL
   32.46     "[| A type;  !!x. x:A ==> b(x) = c(x) : B(x)|] ==> 
   32.47 -   lam x.b(x) = lam x.c(x) : PROD x:A.B(x)"
   32.48 +   lam x. b(x) = lam x. c(x) : PROD x:A. B(x)"
   32.49  
   32.50 -  ProdE  "[| p : PROD x:A.B(x);  a : A |] ==> p`a : B(a)"
   32.51 -  ProdEL "[| p=q: PROD x:A.B(x);  a=b : A |] ==> p`a = q`b : B(a)"
   32.52 +  ProdE  "[| p : PROD x:A. B(x);  a : A |] ==> p`a : B(a)"
   32.53 +  ProdEL "[| p=q: PROD x:A. B(x);  a=b : A |] ==> p`a = q`b : B(a)"
   32.54  
   32.55    ProdC
   32.56     "[| a : A;  !!x. x:A ==> b(x) : B(x)|] ==> 
   32.57 -   (lam x.b(x)) ` a = b(a) : B(a)"
   32.58 +   (lam x. b(x)) ` a = b(a) : B(a)"
   32.59  
   32.60    ProdC2
   32.61 -   "p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)"
   32.62 +   "p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)"
   32.63  
   32.64  
   32.65    (*The Sum of a family of types*)
   32.66  
   32.67 -  SumF  "[| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type"
   32.68 +  SumF  "[| A type;  !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type"
   32.69    SumFL
   32.70 -    "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A.B(x) = SUM x:C.D(x)"
   32.71 +    "[| A = C;  !!x. x:A ==> B(x) = D(x) |] ==> SUM x:A. B(x) = SUM x:C. D(x)"
   32.72  
   32.73 -  SumI  "[| a : A;  b : B(a) |] ==> <a,b> : SUM x:A.B(x)"
   32.74 -  SumIL "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)"
   32.75 +  SumI  "[| a : A;  b : B(a) |] ==> <a,b> : SUM x:A. B(x)"
   32.76 +  SumIL "[| a=c:A;  b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)"
   32.77  
   32.78    SumE
   32.79 -    "[| p: SUM x:A.B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
   32.80 -    ==> split(p, %x y.c(x,y)) : C(p)"
   32.81 +    "[| p: SUM x:A. B(x);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
   32.82 +    ==> split(p, %x y. c(x,y)) : C(p)"
   32.83  
   32.84    SumEL
   32.85 -    "[| p=q : SUM x:A.B(x); 
   32.86 +    "[| p=q : SUM x:A. B(x); 
   32.87         !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)|] 
   32.88 -    ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)"
   32.89 +    ==> split(p, %x y. c(x,y)) = split(q, % x y. d(x,y)) : C(p)"
   32.90  
   32.91    SumC
   32.92      "[| a: A;  b: B(a);  !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>) |] 
   32.93 -    ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)"
   32.94 +    ==> split(<a,b>, %x y. c(x,y)) = c(a,b) : C(<a,b>)"
   32.95  
   32.96 -  fst_def   "fst(a) == split(a, %x y.x)"
   32.97 -  snd_def   "snd(a) == split(a, %x y.y)"
   32.98 +  fst_def   "fst(a) == split(a, %x y. x)"
   32.99 +  snd_def   "snd(a) == split(a, %x y. y)"
  32.100  
  32.101  
  32.102    (*The sum of two types*)
  32.103 @@ -200,22 +200,22 @@
  32.104    PlusE
  32.105      "[| p: A+B;  !!x. x:A ==> c(x): C(inl(x));  
  32.106                  !!y. y:B ==> d(y): C(inr(y)) |] 
  32.107 -    ==> when(p, %x.c(x), %y.d(y)) : C(p)"
  32.108 +    ==> when(p, %x. c(x), %y. d(y)) : C(p)"
  32.109  
  32.110    PlusEL
  32.111      "[| p = q : A+B;  !!x. x: A ==> c(x) = e(x) : C(inl(x));   
  32.112                       !!y. y: B ==> d(y) = f(y) : C(inr(y)) |] 
  32.113 -    ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)"
  32.114 +    ==> when(p, %x. c(x), %y. d(y)) = when(q, %x. e(x), %y. f(y)) : C(p)"
  32.115  
  32.116    PlusC_inl
  32.117      "[| a: A;  !!x. x:A ==> c(x): C(inl(x));  
  32.118                !!y. y:B ==> d(y): C(inr(y)) |] 
  32.119 -    ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))"
  32.120 +    ==> when(inl(a), %x. c(x), %y. d(y)) = c(a) : C(inl(a))"
  32.121  
  32.122    PlusC_inr
  32.123      "[| b: B;  !!x. x:A ==> c(x): C(inl(x));  
  32.124                !!y. y:B ==> d(y): C(inr(y)) |] 
  32.125 -    ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))"
  32.126 +    ==> when(inr(b), %x. c(x), %y. d(y)) = d(b) : C(inr(b))"
  32.127  
  32.128  
  32.129    (*The type Eq*)
    33.1 --- a/src/CTT/ex/elim.ML	Fri Oct 10 16:29:41 1997 +0200
    33.2 +++ b/src/CTT/ex/elim.ML	Fri Oct 10 17:10:12 1997 +0200
    33.3 @@ -148,7 +148,7 @@
    33.4  
    33.5  writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
    33.6  val prems = goal CTT.thy   
    33.7 -    "[| A type;  !!x.x:A ==> B(x) type;                         \
    33.8 +    "[| A type;  !!x. x:A ==> B(x) type;                         \
    33.9  \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
   33.10  \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
   33.11  \                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
    34.1 --- a/src/CTT/ex/equal.ML	Fri Oct 10 16:29:41 1997 +0200
    34.2 +++ b/src/CTT/ex/equal.ML	Fri Oct 10 17:10:12 1997 +0200
    34.3 @@ -24,7 +24,7 @@
    34.4  
    34.5  (*in the "rec" formulation of addition, 0+n=n *)
    34.6  val prems =
    34.7 -goal CTT.thy "p:N ==> rec(p,0, %y z.succ(y)) = p : N";
    34.8 +goal CTT.thy "p:N ==> rec(p,0, %y z. succ(y)) = p : N";
    34.9  by (rtac EqE 1);
   34.10  by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
   34.11  by (rew_tac prems);
   34.12 @@ -33,7 +33,7 @@
   34.13  
   34.14  (*the harder version, n+0=n: recursive, uses induction hypothesis*)
   34.15  val prems =
   34.16 -goal CTT.thy "p:N ==> rec(p,0, %y z.succ(z)) = p : N";
   34.17 +goal CTT.thy "p:N ==> rec(p,0, %y z. succ(z)) = p : N";
   34.18  by (rtac EqE 1);
   34.19  by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
   34.20  by (hyp_rew_tac prems);
   34.21 @@ -43,8 +43,8 @@
   34.22  (*Associativity of addition*)
   34.23  val prems =
   34.24  goal CTT.thy
   34.25 -   "[| a:N;  b:N;  c:N |] ==> rec(rec(a, b, %x y.succ(y)), c, %x y.succ(y)) = \
   34.26 -\                   rec(a, rec(b, c, %x y.succ(y)), %x y.succ(y)) : N";
   34.27 +   "[| a:N;  b:N;  c:N |] ==> rec(rec(a, b, %x y. succ(y)), c, %x y. succ(y)) = \
   34.28 +\                   rec(a, rec(b, c, %x y. succ(y)), %x y. succ(y)) : N";
   34.29  by (NE_tac "a" 1);
   34.30  by (hyp_rew_tac prems);
   34.31  result();
   34.32 @@ -53,7 +53,7 @@
   34.33  (*Martin-Lof (1984) page 62: pairing is surjective*)
   34.34  val prems =
   34.35  goal CTT.thy
   34.36 -    "p : Sum(A,B) ==> <split(p,%x y.x), split(p,%x y.y)> = p : Sum(A,B)";
   34.37 +    "p : Sum(A,B) ==> <split(p,%x y. x), split(p,%x y. y)> = p : Sum(A,B)";
   34.38  by (rtac EqE 1);
   34.39  by (resolve_tac elim_rls 1  THEN  resolve_tac prems 1);
   34.40  by (DEPTH_SOLVE_1 (rew_tac prems));   (*!!!!!!!*)
   34.41 @@ -62,7 +62,7 @@
   34.42  
   34.43  val prems =
   34.44  goal CTT.thy "[| a : A;  b : B |] ==> \
   34.45 -\    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B.A";
   34.46 +\    (lam u. split(u, %v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A";
   34.47  by (rew_tac prems);
   34.48  result();
   34.49  
   34.50 @@ -71,7 +71,7 @@
   34.51  val prems =
   34.52  goal CTT.thy
   34.53     "(lam f. lam x. f`(f`x)) ` (lam u. split(u, %v w.<w,v>)) =  \
   34.54 -\     lam x. x  :  PROD x:(SUM y:N.N). (SUM y:N.N)";
   34.55 +\     lam x. x  :  PROD x:(SUM y:N. N). (SUM y:N. N)";
   34.56  by (resolve_tac reduction_rls 1);
   34.57  by (resolve_tac intrL_rls 3);
   34.58  by (rtac EqE 4);
    35.1 --- a/src/CTT/ex/typechk.ML	Fri Oct 10 16:29:41 1997 +0200
    35.2 +++ b/src/CTT/ex/typechk.ML	Fri Oct 10 17:10:12 1997 +0200
    35.3 @@ -45,17 +45,17 @@
    35.4  result(); 
    35.5  
    35.6  writeln"typechecking an application of fst";
    35.7 -goal CTT.thy "(lam u. split(u, %v w.v)) ` <0, succ(0)> : ?A";
    35.8 +goal CTT.thy "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A";
    35.9  by (typechk_tac[]);
   35.10  result(); 
   35.11  
   35.12  writeln"typechecking the predecessor function";
   35.13 -goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
   35.14 +goal CTT.thy "lam n. rec(n, 0, %x y. x) : ?A";
   35.15  by (typechk_tac[]);
   35.16  result(); 
   35.17  
   35.18  writeln"typechecking the addition function";
   35.19 -goal CTT.thy "lam n. lam m. rec(n, m, %x y.succ(y)) : ?A";
   35.20 +goal CTT.thy "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A";
   35.21  by (typechk_tac[]);
   35.22  result(); 
   35.23  
   35.24 @@ -74,7 +74,7 @@
   35.25  result(); 
   35.26  
   35.27  writeln"typechecking fst (as a function object) ";
   35.28 -goal CTT.thy "lam i. split(i, %j k.j) : ?A";
   35.29 +goal CTT.thy "lam i. split(i, %j k. j) : ?A";
   35.30  by (typechk_tac[]);
   35.31  by N_tac;
   35.32  result(); 
    36.1 --- a/src/LCF/LCF.ML	Fri Oct 10 16:29:41 1997 +0200
    36.2 +++ b/src/LCF/LCF.ML	Fri Oct 10 17:10:12 1997 +0200
    36.3 @@ -65,7 +65,7 @@
    36.4                        REPEAT(rstac(conjI::prems)1)]);
    36.5  
    36.6  val ext = prove_goal thy
    36.7 -        "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))"
    36.8 +        "(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x. f(x))=(%x. g(x))"
    36.9          (fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
   36.10                                      prem RS eq_imp_less1,
   36.11                                      prem RS eq_imp_less2]1)]);
   36.12 @@ -79,7 +79,7 @@
   36.13  val ap_term = refl RS cong;
   36.14  val ap_thm = refl RSN (2,cong);
   36.15  
   36.16 -val UU_abs = prove_goal thy "(%x::'a::cpo.UU) = UU"
   36.17 +val UU_abs = prove_goal thy "(%x::'a::cpo. UU) = UU"
   36.18          (fn _ => [rtac less_anti_sym 1, rtac minimal 2,
   36.19                    rtac less_ext 1, rtac allI 1, rtac minimal 1]);
   36.20  
   36.21 @@ -89,7 +89,7 @@
   36.22          (fn prems=> [rtac less_anti_sym 1,rstac prems 1,rtac minimal 1]);
   36.23  
   36.24  
   36.25 -val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b.P(b)"
   36.26 +val tr_induct = prove_goal thy "[| P(UU); P(TT); P(FF) |] ==> ALL b. P(b)"
   36.27          (fn prems => [rtac allI 1, rtac mp 1,
   36.28                        res_inst_tac[("p","b")]tr_cases 2,
   36.29                        fast_tac (FOL_cs addIs prems) 1]);
    37.1 --- a/src/LCF/LCF.thy	Fri Oct 10 16:29:41 1997 +0200
    37.2 +++ b/src/LCF/LCF.thy	Fri Oct 10 17:10:12 1997 +0200
    37.3 @@ -99,12 +99,12 @@
    37.4       Note that "easiness" of types is not taken into account
    37.5       because it cannot be expressed schematically; flatness could be. *)
    37.6  
    37.7 -  adm_less      "adm(%x.t(x) << u(x))"
    37.8 +  adm_less      "adm(%x. t(x) << u(x))"
    37.9    adm_not_less  "adm(%x.~ t(x) << u)"
   37.10 -  adm_not_free  "adm(%x.A)"
   37.11 -  adm_subst     "adm(P) ==> adm(%x.P(t(x)))"
   37.12 -  adm_conj      "[| adm(P); adm(Q) |] ==> adm(%x.P(x)&Q(x))"
   37.13 -  adm_disj      "[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
   37.14 -  adm_imp       "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
   37.15 -  adm_all       "(!!y.adm(P(y))) ==> adm(%x.ALL y.P(y,x))"
   37.16 +  adm_not_free  "adm(%x. A)"
   37.17 +  adm_subst     "adm(P) ==> adm(%x. P(t(x)))"
   37.18 +  adm_conj      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)&Q(x))"
   37.19 +  adm_disj      "[| adm(P); adm(Q) |] ==> adm(%x. P(x)|Q(x))"
   37.20 +  adm_imp       "[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x. P(x)-->Q(x))"
   37.21 +  adm_all       "(!!y. adm(P(y))) ==> adm(%x. ALL y. P(y,x))"
   37.22  end
    38.1 --- a/src/LCF/fix.ML	Fri Oct 10 16:29:41 1997 +0200
    38.2 +++ b/src/LCF/fix.ML	Fri Oct 10 17:10:12 1997 +0200
    38.3 @@ -22,7 +22,7 @@
    38.4  structure Fix:FIX =
    38.5  struct
    38.6  
    38.7 -val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=(u(x)::'a::cpo))"
    38.8 +val adm_eq = prove_goal LCF.thy "adm(%x. t(x)=(u(x)::'a::cpo))"
    38.9          (fn _ => [rewtac eq_def,
   38.10                    REPEAT(rstac[adm_conj,adm_less]1)]);
   38.11  
   38.12 @@ -41,7 +41,7 @@
   38.13  val not_eq_UU = prove_goal LCF.thy "ALL p. ~p=UU <-> (p=TT | p=FF)"
   38.14      (fn _ => [tac]) RS spec;
   38.15  
   38.16 -val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr.adm(%x. ~t(x)=p)"
   38.17 +val adm_not_eq_tr = prove_goal LCF.thy "ALL p::tr. adm(%x. ~t(x)=p)"
   38.18      (fn _ => [rtac tr_induct 1,
   38.19      REPEAT(simp_tac (LCF_ss addsimps [not_eq_TT,not_eq_FF,not_eq_UU]) 1 THEN
   38.20             REPEAT(rstac [adm_disj,adm_eq] 1))]) RS spec;
   38.21 @@ -80,7 +80,7 @@
   38.22  val FIX2 = FIX_pair_conj RS conjunct2;
   38.23  
   38.24  val induct2 = prove_goal LCF.thy
   38.25 -         "[| adm(%p.P(FST(p),SND(p))); P(UU::'a,UU::'b);\
   38.26 +         "[| adm(%p. P(FST(p),SND(p))); P(UU::'a,UU::'b);\
   38.27  \            ALL x y. P(x,y) --> P(f(x),g(y)) |] ==> P(FIX(f),FIX(g))"
   38.28          (fn prems => [EVERY1
   38.29          [res_inst_tac [("f","f"),("g","g")] (standard(FIX1 RS ssubst)),