# HG changeset patch
# User paulson
# Date 990449506 -7200
# Node ID 8b84ee2cc79cf545c14f1ed0f5097b80ed09d5a4
# Parent  6536fb8c9fc6d6abcfa5e7fdd6500900d3c559b7
X-symbols for ZF

diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Confluence.thy
--- a/src/ZF/Resid/Confluence.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Confluence.thy	Mon May 21 14:51:46 2001 +0200
@@ -13,9 +13,9 @@
 
 defs
   confluence_def "confluence(R) ==   
-                  ALL x y. <x,y>:R --> (ALL z.<x,z>:R -->   
-                                         (EX u.<y,u>:R & <z,u>:R))"
-  strip_def      "strip == ALL x y. (x ===> y) --> (ALL z.(x =1=> z) -->   
-                                         (EX u.(y =1=> u) & (z===>u)))" 
+                  \\<forall>x y. <x,y>:R --> (\\<forall>z.<x,z>:R -->   
+                                         (\\<exists>u.<y,u>:R & <z,u>:R))"
+  strip_def      "strip == \\<forall>x y. (x ===> y) --> (\\<forall>z.(x =1=> z) -->   
+                                         (\\<exists>u.(y =1=> u) & (z===>u)))" 
 end
 
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Conversion.ML
--- a/src/ZF/Resid/Conversion.ML	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Conversion.ML	Mon May 21 14:51:46 2001 +0200
@@ -19,7 +19,7 @@
 (*      Church_Rosser Theorem                                                *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "m<--->n ==> EX p.(m --->p) & (n ---> p)";
+Goal "m<--->n ==> \\<exists>p.(m --->p) & (n ---> p)";
 by (etac Sconv.induct 1);
 by (etac Sconv1.induct 1);
 by (blast_tac (claset() addIs [red1D1,redD2]) 1);
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Conversion.thy
--- a/src/ZF/Resid/Conversion.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Conversion.thy	Mon May 21 14:51:46 2001 +0200
@@ -29,7 +29,7 @@
   domains       "Sconv" <= "lambda*lambda"
   intrs
     one_step    "m<-1->n  ==> m<--->n"
-    refl        "m:lambda ==> m<--->m"
+    refl        "m \\<in> lambda ==> m<--->m"
     trans       "[|m<--->n; n<--->p|] ==> m<--->p"
   type_intrs    "[Sconv1.dom_subset RS subsetD]@lambda.intrs@bool_typechecks"
 end
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Cube.ML
--- a/src/ZF/Resid/Cube.ML	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Cube.ML	Mon May 21 14:51:46 2001 +0200
@@ -15,7 +15,7 @@
 
 (* Having more assumptions than needed -- removed below  *)
 Goal "v<==u ==> \
-\   regular(u) --> (ALL w. w~v --> w~u -->  \
+\   regular(u) --> (\\<forall>w. w~v --> w~u -->  \
 \                          w |> u = (w|>v) |> (u|>v))";
 by (etac Ssub.induct 1);
 by Auto_tac;
@@ -56,7 +56,7 @@
 (* ------------------------------------------------------------------------- *)
 
 Goal "[|w~u; w~v; regular(u); regular(v)|]==> \
-\          EX uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
+\          \\<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
 \            regular(vu) & (w|>v)~uv & regular(uv) ";
 by (subgoal_tac "u~v" 1);
 by (safe_tac (claset() addSIs [exI]));
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Redex.ML
--- a/src/ZF/Resid/Redex.ML	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Redex.ML	Mon May 21 14:51:46 2001 +0200
@@ -21,15 +21,15 @@
 (*    Equality rules for union                                               *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "n:nat==>Var(n) un Var(n)=Var(n)";
+Goal "n \\<in> nat==>Var(n) un Var(n)=Var(n)";
 by (asm_simp_tac (simpset() addsimps [union_def]) 1);
 qed "union_Var";
 
-Goal "[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
+Goal "[|u \\<in> redexes; v \\<in> redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
 by (asm_simp_tac (simpset() addsimps [union_def]) 1);
 qed "union_Fun";
  
-Goal "[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
+Goal "[|b1 \\<in> bool; b2 \\<in> bool; u1 \\<in> redexes; v1 \\<in> redexes; u2 \\<in> redexes; v2 \\<in> redexes|]==> \
 \     App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
 by (asm_simp_tac (simpset() addsimps [union_def]) 1);
 qed "union_App";
@@ -58,7 +58,7 @@
 (*    comp proofs                                                            *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "u:redexes ==> u ~ u";
+Goal "u \\<in> redexes ==> u ~ u";
 by (etac redexes.induct 1);
 by (ALLGOALS Fast_tac);
 qed "comp_refl";
@@ -73,7 +73,7 @@
 qed "comp_sym_iff";
 
 
-Goal "u ~ v ==> ALL w. v ~ w-->u ~ w";
+Goal "u ~ v ==> \\<forall>w. v ~ w-->u ~ w";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
 qed_spec_mp "comp_trans";
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Redex.thy	Mon May 21 14:51:46 2001 +0200
@@ -10,9 +10,9 @@
   redexes     :: i
 
 datatype
-  "redexes" = Var ("n: nat")            
-            | Fun ("t: redexes")
-            | App ("b:bool" ,"f:redexes" , "a:redexes")
+  "redexes" = Var ("n \\<in> nat")            
+            | Fun ("t \\<in> redexes")
+            | App ("b \\<in> bool" ,"f \\<in> redexes" , "a \\<in> redexes")
 
 
 consts
@@ -25,19 +25,19 @@
 translations
   "a<==b"        == "<a,b>:Ssub"
   "a ~ b"        == "<a,b>:Scomp"
-  "regular(a)"   == "a:Sreg"
+  "regular(a)"   == "a \\<in> Sreg"
 
 
 primrec (*explicit lambda is required because both arguments of "un" vary*)
   "union_aux(Var(n)) =
-     (lam t:redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
+     (\\<lambda>t \\<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
 
   "union_aux(Fun(u)) =
-     (lam t:redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
+     (\\<lambda>t \\<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
 	 			  %b y z. 0, t))"
 
   "union_aux(App(b,f,a)) =
-     (lam t:redexes.
+     (\\<lambda>t \\<in> redexes.
         redexes_case(%j. 0, %y. 0,
 		     %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
 
@@ -48,9 +48,9 @@
 inductive
   domains       "Ssub" <= "redexes*redexes"
   intrs
-    Sub_Var     "n:nat ==> Var(n)<== Var(n)"
+    Sub_Var     "n \\<in> nat ==> Var(n)<== Var(n)"
     Sub_Fun     "[|u<== v|]==> Fun(u)<== Fun(v)"
-    Sub_App1    "[|u1<== v1; u2<== v2; b:bool|]==>   
+    Sub_App1    "[|u1<== v1; u2<== v2; b \\<in> bool|]==>   
                      App(0,u1,u2)<== App(b,v1,v2)"
     Sub_App2    "[|u1<== v1; u2<== v2|]==>   
                      App(1,u1,u2)<== App(1,v1,v2)"
@@ -59,16 +59,16 @@
 inductive
   domains       "Scomp" <= "redexes*redexes"
   intrs
-    Comp_Var    "n:nat ==> Var(n) ~ Var(n)"
+    Comp_Var    "n \\<in> nat ==> Var(n) ~ Var(n)"
     Comp_Fun    "[|u ~ v|]==> Fun(u) ~ Fun(v)"
-    Comp_App    "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>   
+    Comp_App    "[|u1 ~ v1; u2 ~ v2; b1 \\<in> bool; b2 \\<in> bool|]==>   
                      App(b1,u1,u2) ~ App(b2,v1,v2)"
   type_intrs    "redexes.intrs@bool_typechecks"
 
 inductive
   domains       "Sreg" <= "redexes"
   intrs
-    Reg_Var     "n:nat ==> regular(Var(n))"
+    Reg_Var     "n \\<in> nat ==> regular(Var(n))"
     Reg_Fun     "[|regular(u)|]==> regular(Fun(u))"
     Reg_App1    "[|regular(Fun(u)); regular(v) 
                      |]==>regular(App(1,Fun(u),v))"
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Reduction.ML
--- a/src/ZF/Resid/Reduction.ML	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Reduction.ML	Mon May 21 14:51:46 2001 +0200
@@ -39,13 +39,13 @@
 by (ALLGOALS (Asm_simp_tac ));
 qed "red_Fun";
 
-Goal "[|n:lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
+Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
 by (etac Sred.induct 1);
 by (resolve_tac [Sred.trans] 3);
 by (ALLGOALS (Asm_simp_tac ));
 qed "red_Apll";
 
-Goal "[|n:lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
+Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
 by (etac Sred.induct 1);
 by (resolve_tac [Sred.trans] 3);
 by (ALLGOALS (Asm_simp_tac ));
@@ -56,7 +56,7 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apll,red_Aplr]) ));
 qed "red_Apl";
 
-Goal "[|m:lambda; m':lambda; n:lambda; n':lambda; m ---> m'; n--->n'|]==> \
+Goal "[|m \\<in> lambda; m':lambda; n \\<in> lambda; n':lambda; m ---> m'; n--->n'|]==> \
 \              Apl(Fun(m),n)---> n'/m'";
 by (res_inst_tac [("n","Apl(Fun(m'),n')")] Sred.trans 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apl,red_Fun]) ));
@@ -68,7 +68,7 @@
 (* ------------------------------------------------------------------------- *)
 
 
-Goal "m:lambda==> m =1=> m";
+Goal "m \\<in> lambda==> m =1=> m";
 by (etac lambda.induct 1);
 by (ALLGOALS (Asm_simp_tac ));
 qed "refl_par_red1";
@@ -96,7 +96,7 @@
 (*      Simulation                                                           *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "m=1=>n ==> EX v. m|>v = n & m~v & regular(v)";
+Goal "m=1=>n ==> \\<exists>v. m|>v = n & m~v & regular(v)";
 by (etac Spar_red1.induct 1);
 by Safe_tac;
 by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
@@ -109,12 +109,12 @@
 (*           commuting of unmark and subst                                   *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "u:redexes ==> ALL k:nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
+Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
 by (etac redexes.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
 qed "unmmark_lift_rec";
 
-Goal "v:redexes ==> ALL k:nat. ALL u:redexes.  \
+Goal "v \\<in> redexes ==> \\<forall>k \\<in> nat. \\<forall>u \\<in> redexes.  \
 \         unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
 by (etac redexes.induct 1);
 by (ALLGOALS (asm_simp_tac 
@@ -134,7 +134,7 @@
 by Auto_tac;
 qed_spec_mp "completeness_l";
 
-Goal "[|u:lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
+Goal "[|u \\<in> lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
 by (dtac completeness_l 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lambda_unmark]) ));
 qed "completeness";
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Reduction.thy	Mon May 21 14:51:46 2001 +0200
@@ -21,11 +21,11 @@
 inductive
   domains       "Sred1" <= "lambda*lambda"
   intrs
-    beta        "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m"
+    beta        "[|m \\<in> lambda; n \\<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
     rfun        "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
-    apl_l       "[|m2:lambda; m1 -1-> n1|] ==>   
+    apl_l       "[|m2 \\<in> lambda; m1 -1-> n1|] ==>   
                                   Apl(m1,m2) -1-> Apl(n1,m2)"
-    apl_r       "[|m1:lambda; m2 -1-> n2|] ==>   
+    apl_r       "[|m1 \\<in> lambda; m2 -1-> n2|] ==>   
                                   Apl(m1,m2) -1-> Apl(m1,n2)"
   type_intrs    "red_typechecks"
 
@@ -33,7 +33,7 @@
   domains       "Sred" <= "lambda*lambda"
   intrs
     one_step    "[|m-1->n|] ==> m--->n"
-    refl        "m:lambda==>m --->m"
+    refl        "m \\<in> lambda==>m --->m"
     trans       "[|m--->n; n--->p|]==>m--->p"
   type_intrs    "[Sred1.dom_subset RS subsetD]@red_typechecks"
 
@@ -42,7 +42,7 @@
   intrs
     beta        "[|m =1=> m';   
                  n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
-    rvar        "n:nat==> Var(n) =1=> Var(n)"
+    rvar        "n \\<in> nat==> Var(n) =1=> Var(n)"
     rfun        "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
     rapl        "[|m =1=> m';   
                  n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Residuals.ML
--- a/src/ZF/Resid/Residuals.ML	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Residuals.ML	Mon May 21 14:51:46 2001 +0200
@@ -41,12 +41,12 @@
 (*       residuals is a  partial function                                    *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "residuals(u,v,w) ==> ALL w1. residuals(u,v,w1) --> w1 = w";
+Goal "residuals(u,v,w) ==> \\<forall>w1. residuals(u,v,w1) --> w1 = w";
 by (etac Sres.induct 1);
 by (ALLGOALS Force_tac);
 qed_spec_mp "residuals_function";
 
-Goal "u~v ==> regular(v) --> (EX w. residuals(u,v,w))";
+Goal "u~v ==> regular(v) --> (\\<exists>w. residuals(u,v,w))";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
 qed "residuals_intro";
@@ -62,7 +62,7 @@
 (*               Residual function                                           *)
 (* ------------------------------------------------------------------------- *)
 
-Goalw [res_func_def] "n:nat ==> Var(n) |> Var(n) = Var(n)";
+Goalw [res_func_def] "n \\<in> nat ==> Var(n) |> Var(n) = Var(n)";
 by (Blast_tac 1);
 qed "res_Var";
 
@@ -73,25 +73,25 @@
 qed "res_Fun";
 
 Goalw [res_func_def]
-    "[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
+    "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
 \           App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)";
 by (blast_tac (claset() addSDs [comp_resfuncD]
 			addIs [residuals_function]) 1);
 qed "res_App";
 
 Goalw [res_func_def]
-    "[|s~u; regular(u); t~v; regular(v); b:bool|]==> \
+    "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
 \           App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
 by (blast_tac (claset() addSEs redexes.free_SEs
 			addSDs [comp_resfuncD]
 			addIs [residuals_function]) 1);
 qed "res_redex";
 
-Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t:redexes";
+Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t \\<in> redexes";
 by (etac Scomp.induct 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [res_Var,res_Fun,res_App,res_redex]));
-by (dres_inst_tac [("psi", "Fun(?u) |> ?v : redexes")] asm_rl 1);
+by (dres_inst_tac [("psi", "Fun(?u) |> ?v \\<in> redexes")] asm_rl 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [res_Fun]));
 qed "resfunc_type";
@@ -115,7 +115,7 @@
 by Auto_tac;
 qed_spec_mp "sub_preserve_reg";
 
-Goal "[|u~v; k:nat|]==> regular(v)--> (ALL n:nat.  \
+Goal "[|u~v; k \\<in> nat|]==> regular(v)--> (\\<forall>n \\<in> nat.  \
 \        lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))";
 by (etac Scomp.induct 1);
 by Safe_tac;
@@ -126,15 +126,15 @@
 by (Asm_full_simp_tac 1);
 qed "residuals_lift_rec";
 
-Goal "u1~u2 ==>  ALL v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
-\   (ALL n:nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
+Goal "u1~u2 ==>  \\<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
+\   (\\<forall>n \\<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
 \              subst_rec(v1 |> v2, u1 |> u2,n))";
 by (etac Scomp.induct 1);
 by Safe_tac;
 by (ALLGOALS
     (asm_simp_tac
      (simpset() addsimps [lift_rec_Var,subst_Var,residuals_lift_rec])));
-by (dres_inst_tac [("psi", "ALL x.?P(x)")] asm_rl 1);
+by (dres_inst_tac [("psi", "\\<forall>x.?P(x)")] asm_rl 1);
 by (asm_full_simp_tac (simpset() addsimps [substitution]) 1);
 qed "residuals_subst_rec";
 
@@ -148,7 +148,7 @@
 (*     Residuals are comp and regular                                        *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
+Goal "u~v ==> \\<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
 by (etac Scomp.induct 1);
 by (ALLGOALS Force_tac);
 qed_spec_mp "residuals_preserve_comp";
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Residuals.thy	Mon May 21 14:51:46 2001 +0200
@@ -19,14 +19,14 @@
 inductive
   domains       "Sres" <= "redexes*redexes*redexes"
   intrs
-    Res_Var     "n:nat ==> residuals(Var(n),Var(n),Var(n))"
+    Res_Var     "n \\<in> nat ==> residuals(Var(n),Var(n),Var(n))"
     Res_Fun     "[|residuals(u,v,w)|]==>   
                      residuals(Fun(u),Fun(v),Fun(w))"
     Res_App     "[|residuals(u1,v1,w1);   
-                   residuals(u2,v2,w2); b:bool|]==>   
+                   residuals(u2,v2,w2); b \\<in> bool|]==>   
                  residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
     Res_redex   "[|residuals(u1,v1,w1);   
-                   residuals(u2,v2,w2); b:bool|]==>   
+                   residuals(u2,v2,w2); b \\<in> bool|]==>   
                  residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
   type_intrs    "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
 
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Substitution.ML
--- a/src/ZF/Resid/Substitution.ML	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Substitution.ML	Mon May 21 14:51:46 2001 +0200
@@ -9,23 +9,23 @@
 (*   Arithmetic extensions                                                   *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "[| p < n; n:nat|] ==> n~=p";
+Goal "[| p < n; n \\<in> nat|] ==> n\\<noteq>p";
 by (Fast_tac 1);
 qed "gt_not_eq";
 
-Goal "[|j:nat; i:nat|] ==> i < j --> succ(j #- 1) = j";
+Goal "[|j \\<in> nat; i \\<in> nat|] ==> i < j --> succ(j #- 1) = j";
 by (induct_tac "j" 1);
 by (Fast_tac 1);
 by (Asm_simp_tac 1);
 qed "succ_pred";
 
-Goal "[|succ(x)<n; n:nat; x:nat|] ==> x < n #- 1 ";
+Goal "[|succ(x)<n; n \\<in> nat; x \\<in> nat|] ==> x < n #- 1 ";
 by (rtac succ_leE 1);
 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
 qed "lt_pred";
 
-Goal "[|n < succ(x); p<n; p:nat; n:nat; x:nat|] ==> n #- 1 < x ";
+Goal "[|n < succ(x); p<n; p \\<in> nat; n \\<in> nat; x \\<in> nat|] ==> n #- 1 < x ";
 by (rtac succ_leE 1);
 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
 qed "gt_pred";
@@ -37,25 +37,25 @@
 (* ------------------------------------------------------------------------- *)
 (*     lift_rec equality rules                                               *)
 (* ------------------------------------------------------------------------- *)
-Goal "[|n:nat; i:nat|] \
+Goal "[|n \\<in> nat; i \\<in> nat|] \
 \     ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))";
 by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
 qed "lift_rec_Var";
 
-Goal "[|n:nat; i:nat; k:nat; k le i|] ==> lift_rec(Var(i),k) = Var(succ(i))";
+Goal "[|n \\<in> nat; i \\<in> nat; k \\<in> nat; k le i|] ==> lift_rec(Var(i),k) = Var(succ(i))";
 by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
 qed "lift_rec_le";
 
-Goal "[|i:nat; k:nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)";
+Goal "[|i \\<in> nat; k \\<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)";
 by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
 qed "lift_rec_gt";
 
-Goal "[|n:nat; k:nat|] ==>   \
+Goal "[|n \\<in> nat; k \\<in> nat|] ==>   \
 \        lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
 by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
 qed "lift_rec_Fun";
 
-Goal "[|n:nat; k:nat|] ==>   \
+Goal "[|n \\<in> nat; k \\<in> nat|] ==>   \
 \        lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
 by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
 qed "lift_rec_App";
@@ -65,32 +65,32 @@
 (*    substitution quality rules                                             *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "[|i:nat; k:nat; u:redexes|]  \
+Goal "[|i \\<in> nat; k \\<in> nat; u \\<in> redexes|]  \
 \     ==> subst_rec(u,Var(i),k) =  \
 \         (if k<i then Var(i #- 1) else if k=i then u else Var(i))";
 by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
 qed "subst_Var";
 
-Goal "[|n:nat; u:redexes|] ==> subst_rec(u,Var(n),n) = u";
+Goal "[|n \\<in> nat; u \\<in> redexes|] ==> subst_rec(u,Var(n),n) = u";
 by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
 qed "subst_eq";
 
-Goal "[|n:nat; u:redexes; p:nat; p<n|] ==>  \
+Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; p<n|] ==>  \
 \     subst_rec(u,Var(n),p) = Var(n #- 1)";
 by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
 qed "subst_gt";
 
-Goal "[|n:nat; u:redexes; p:nat; n<p|] ==>  \
+Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; n<p|] ==>  \
 \     subst_rec(u,Var(n),p) = Var(n)";
 by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
 qed "subst_lt";
 
-Goal "[|p:nat; u:redexes|] ==>  \
+Goal "[|p \\<in> nat; u \\<in> redexes|] ==>  \
 \     subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
 by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
 qed "subst_Fun";
 
-Goal "[|p:nat; u:redexes|] ==>  \
+Goal "[|p \\<in> nat; u \\<in> redexes|] ==>  \
 \     subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
 by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
 qed "subst_App";
@@ -99,14 +99,14 @@
 Addsimps [subst_Fun, subst_App];
 
 
-Goal "u:redexes ==> ALL k:nat. lift_rec(u,k):redexes";
+Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. lift_rec(u,k):redexes";
 by (etac redexes.induct 1);
 by (ALLGOALS
     (asm_simp_tac (simpset() addsimps [lift_rec_Var,
 				       lift_rec_Fun, lift_rec_App])));
 qed_spec_mp "lift_rec_type";
 
-Goal "v:redexes ==>  ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
+Goal "v \\<in> redexes ==>  \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. subst_rec(u,v,n):redexes";
 by (etac redexes.induct 1);
 by (ALLGOALS(asm_simp_tac 
     (simpset() addsimps [subst_Var, lift_rec_type])));
@@ -122,7 +122,7 @@
 (*    lift and  substitution proofs                                          *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "u:redexes ==> ALL n:nat. ALL i:nat. i le n -->   \
+Goal "u \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>i \\<in> nat. i le n -->   \
 \       (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
 by (etac redexes.induct 1);
 by (ALLGOALS Asm_simp_tac);
@@ -132,13 +132,13 @@
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
 qed "lift_lift_rec";
 
-Goal "[|u:redexes; n:nat|] ==>  \
+Goal "[|u \\<in> redexes; n \\<in> nat|] ==>  \
 \      lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
 by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1);
 qed "lift_lift";
 
-Goal "v:redexes ==>  \
-\      ALL n:nat. ALL m:nat. ALL u:redexes. n le m-->\
+Goal "v \\<in> redexes ==>  \
+\      \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. n le m-->\
 \         lift_rec(subst_rec(u,v,n),m) = \
 \              subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
 by ((etac redexes.induct 1)
@@ -157,14 +157,14 @@
 by (asm_simp_tac (simpset() addsimps [leI]) 1);
 qed "lift_rec_subst_rec";
 
-Goal "[|v:redexes; u:redexes; n:nat|] ==>  \
+Goal "[|v \\<in> redexes; u \\<in> redexes; n \\<in> nat|] ==>  \
 \        lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
 by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
 qed "lift_subst";
 
 
-Goal "v:redexes ==>  \
-\      ALL n:nat. ALL m:nat. ALL u:redexes. m le n-->\
+Goal "v \\<in> redexes ==>  \
+\      \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. m le n-->\
 \         lift_rec(subst_rec(u,v,n),m) = \
 \              subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
 by (etac redexes.induct 1
@@ -183,16 +183,16 @@
 qed "lift_rec_subst_rec_lt";
 
 
-Goal "u:redexes ==>  \
-\       ALL n:nat. ALL v:redexes. subst_rec(v,lift_rec(u,n),n) =  u";
+Goal "u \\<in> redexes ==>  \
+\       \\<forall>n \\<in> nat. \\<forall>v \\<in> redexes. subst_rec(v,lift_rec(u,n),n) =  u";
 by (etac redexes.induct 1);
 by Auto_tac;
 by (case_tac "n < x" 1);
 by Auto_tac;
 qed "subst_rec_lift_rec";
 
-Goal "v:redexes ==>  \
-\       ALL m:nat. ALL n:nat. ALL u:redexes. ALL w:redexes. m le  n --> \
+Goal "v \\<in> redexes ==>  \
+\       \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. \\<forall>w \\<in> redexes. m le  n --> \
 \    subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
 \    subst_rec(w,subst_rec(u,v,m),n)";
 by (etac redexes.induct 1);
@@ -220,7 +220,7 @@
 qed "subst_rec_subst_rec";
 
 
-Goal "[|v:redexes; u:redexes; w:redexes; n:nat|] ==>  \
+Goal "[|v \\<in> redexes; u \\<in> redexes; w \\<in> redexes; n \\<in> nat|] ==>  \
 \       subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)";
 by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1);
 qed "substitution";
@@ -231,12 +231,12 @@
 (* ------------------------------------------------------------------------- *)
 
 
-Goal "[|n:nat; u ~ v|] ==> ALL m:nat. lift_rec(u,m) ~ lift_rec(v,m)";
+Goal "[|n \\<in> nat; u ~ v|] ==> \\<forall>m \\<in> nat. lift_rec(u,m) ~ lift_rec(v,m)";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl])));
 qed "lift_rec_preserve_comp";
 
-Goal "u2 ~ v2 ==> ALL m:nat. ALL u1:redexes. ALL v1:redexes.\
+Goal "u2 ~ v2 ==> \\<forall>m \\<in> nat. \\<forall>u1 \\<in> redexes. \\<forall>v1 \\<in> redexes.\
 \            u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
 by (etac Scomp.induct 1);
 by (ALLGOALS
@@ -244,13 +244,13 @@
      (simpset() addsimps [subst_Var, lift_rec_preserve_comp, comp_refl])));
 qed "subst_rec_preserve_comp";
 
-Goal "regular(u) ==> ALL m:nat. regular(lift_rec(u,m))";
+Goal "regular(u) ==> \\<forall>m \\<in> nat. regular(lift_rec(u,m))";
 by (etac Sreg.induct 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var])));
 qed "lift_rec_preserve_reg";
 
 Goal "regular(v) ==>  \
-\       ALL m:nat. ALL u:redexes. regular(u)-->regular(subst_rec(u,v,m))";
+\       \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. regular(u)-->regular(subst_rec(u,v,m))";
 by (etac Sreg.induct 1);
 by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_Var,
 						    lift_rec_preserve_reg])));
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Substitution.thy	Mon May 21 14:51:46 2001 +0200
@@ -29,23 +29,23 @@
     in the recursive calls ***)
 
 primrec
-  "lift_aux(Var(i)) = (lam k:nat. if i<k then Var(i) else Var(succ(i)))"
+  "lift_aux(Var(i)) = (\\<lambda>k \\<in> nat. if i<k then Var(i) else Var(succ(i)))"
 
-  "lift_aux(Fun(t)) = (lam k:nat. Fun(lift_aux(t) ` succ(k)))"
+  "lift_aux(Fun(t)) = (\\<lambda>k \\<in> nat. Fun(lift_aux(t) ` succ(k)))"
 
-  "lift_aux(App(b,f,a)) = (lam k:nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
+  "lift_aux(App(b,f,a)) = (\\<lambda>k \\<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
 
 
   
 primrec
   "subst_aux(Var(i)) =
-     (lam r:redexes. lam k:nat. if k<i then Var(i #- 1) 
+     (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. if k<i then Var(i #- 1) 
 				else if k=i then r else Var(i))"
   "subst_aux(Fun(t)) =
-     (lam r:redexes. lam k:nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
+     (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
 
   "subst_aux(App(b,f,a)) = 
-     (lam r:redexes. lam k:nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
+     (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
 
 end
 
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Terms.ML
--- a/src/ZF/Resid/Terms.ML	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Terms.ML	Mon May 21 14:51:46 2001 +0200
@@ -12,12 +12,12 @@
 (*        unmark lemmas                                                      *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "u:redexes ==> unmark(u):lambda";
+Goal "u \\<in> redexes ==> unmark(u):lambda";
 by (etac redexes.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "unmark_type";
 
-Goal "u:lambda ==> unmark(u) = u";
+Goal "u \\<in> lambda ==> unmark(u) = u";
 by (etac lambda.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "lambda_unmark";
@@ -27,12 +27,12 @@
 (*         lift and subst preserve lambda                                    *)
 (* ------------------------------------------------------------------------- *)
 
-Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
+Goal "v \\<in> lambda ==> \\<forall>k \\<in> nat. lift_rec(v,k):lambda";
 by (etac lambda.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
 qed_spec_mp "liftL_type";
 
-Goal "v:lambda ==>  ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
+Goal "v \\<in> lambda ==>  \\<forall>n \\<in> nat. \\<forall>u \\<in> lambda. subst_rec(u,v,n):lambda";
 by (etac lambda.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
 qed_spec_mp "substL_type";
diff -r 6536fb8c9fc6 -r 8b84ee2cc79c src/ZF/Resid/Terms.thy
--- a/src/ZF/Resid/Terms.thy	Mon May 21 14:46:30 2001 +0200
+++ b/src/ZF/Resid/Terms.thy	Mon May 21 14:51:46 2001 +0200
@@ -18,9 +18,9 @@
 inductive
   domains       "lambda" <= "redexes"
   intrs
-    Lambda_Var  "               n:nat ==>     Var(n):lambda"
-    Lambda_Fun  "            u:lambda ==>     Fun(u):lambda"
-    Lambda_App  "[|u:lambda; v:lambda|]==> Apl(u,v):lambda"
+    Lambda_Var  "               n \\<in> nat ==>     Var(n):lambda"
+    Lambda_Fun  "            u \\<in> lambda ==>     Fun(u):lambda"
+    Lambda_App  "[|u \\<in> lambda; v \\<in> lambda|]==> Apl(u,v):lambda"
   type_intrs    "redexes.intrs@bool_typechecks"
 
 primrec