isabelle: changeset 11316:b4e71bd751e4

--- a/src/ZF/ex/Acc.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Acc.ML	Mon May 21 14:36:24 2001 +0200
@@ -9,23 +9,23 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-(*The introduction rule must require  a:field(r)  
+(*The introduction rule must require  a \\<in> field(r)  
   Otherwise acc(r) would be a proper class!    *)
 
 (*The intended introduction rule*)
 val prems = goal Acc.thy
-    "[| !!b. <b,a>:r ==> b: acc(r);  a: field(r) |] ==> a: acc(r)";
+    "[| !!b. <b,a>:r ==> b \\<in> acc(r);  a \\<in> field(r) |] ==> a \\<in> acc(r)";
 by (fast_tac (claset() addIs prems@acc.intrs) 1);
 qed "accI";
 
-Goal "[| b: acc(r);  <a,b>: r |] ==> a: acc(r)";
+Goal "[| b \\<in> acc(r);  <a,b>: r |] ==> a \\<in> acc(r)";
 by (etac acc.elim 1);
 by (Fast_tac 1);
 qed "acc_downward";
 
 val [major,indhyp] = goal Acc.thy
-    "[| a : acc(r);                                             \
-\       !!x. [| x: acc(r);  ALL y. <y,x>:r --> P(y) |] ==> P(x) \
+    "[| a \\<in> acc(r);                                             \
+\       !!x. [| x \\<in> acc(r);  \\<forall>y. <y,x>:r --> P(y) |] ==> P(x) \
 \    |] ==> P(a)";
 by (rtac (major RS acc.induct) 1);
 by (rtac indhyp 1);
@@ -41,10 +41,10 @@
 by (Fast_tac 1);
 qed "wf_on_acc";
 
-(* field(r) <= acc(r) ==> wf(r) *)
+(* field(r) \\<subseteq> acc(r) ==> wf(r) *)
 val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf;
 
-val [major] = goal Acc.thy "wf(r) ==> field(r) <= acc(r)";
+val [major] = goal Acc.thy "wf(r) ==> field(r) \\<subseteq> acc(r)";
 by (rtac subsetI 1);
 by (etac (major RS wf_induct2) 1);
 by (rtac subset_refl 1);
@@ -53,6 +53,6 @@
 by (Fast_tac 1);
 qed "acc_wfD";
 
-Goal "wf(r) <-> field(r) <= acc(r)";
+Goal "wf(r) <-> field(r) \\<subseteq> acc(r)";
 by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
 qed "wf_acc_iff";

--- a/src/ZF/ex/Acc.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Acc.thy	Mon May 21 14:36:24 2001 +0200
@@ -17,7 +17,7 @@
 inductive
   domains "acc(r)" <= "field(r)"
   intrs
-    vimage  "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
+    vimage  "[| r-``{a}: Pow(acc(r)); a \\<in> field(r) |] ==> a \\<in> acc(r)"
   monos      Pow_mono
 
 end

--- a/src/ZF/ex/BT.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/BT.ML	Mon May 21 14:36:24 2001 +0200
@@ -8,7 +8,7 @@
 
 Addsimps bt.intrs;
 
-Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
+Goal "l \\<in> bt(A) ==> \\<forall>x r. Br(x,l,r) \\<noteq> l";
 by (induct_tac "l" 1);
 by Auto_tac;
 qed_spec_mp "Br_neq_left";
@@ -17,17 +17,17 @@
 val Br_iff = bt.mk_free "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'";
 
 (*An elimination rule, for type-checking*)
-val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
+val BrE = bt.mk_cases "Br(a,l,r) \\<in> bt(A)";
 
 (**  Lemmas to justify using "bt" in other recursive type definitions **)
 
-Goalw bt.defs "A<=B ==> bt(A) <= bt(B)";
+Goalw bt.defs "A \\<subseteq> B ==> bt(A) \\<subseteq> bt(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac bt.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
 qed "bt_mono";
 
-Goalw (bt.defs@bt.con_defs) "bt(univ(A)) <= univ(A)";
+Goalw (bt.defs@bt.con_defs) "bt(univ(A)) \\<subseteq> univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac (A_subset_univ RS univ_mono) 2);
 by (fast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
@@ -39,19 +39,19 @@
 
 (*Type checking for recursor -- example only; not really needed*)
 val major::prems = goal BT.thy
-    "[| t: bt(A);    \
-\       c: C(Lf);       \
-\       !!x y z r s. [| x:A;  y:bt(A);  z:bt(A);  r:C(y);  s:C(z) |] ==> \
+    "[| t \\<in> bt(A);    \
+\       c \\<in> C(Lf);       \
+\       !!x y z r s. [| x \\<in> A;  y \\<in> bt(A);  z \\<in> bt(A);  r \\<in> C(y);  s \\<in> C(z) |] ==> \
 \                    h(x,y,z,r,s): C(Br(x,y,z))  \
-\    |] ==> bt_rec(c,h,t) : C(t)";
-    (*instead of induct_tac "t", since t: bt(A) isn't an assumption*)
+\    |] ==> bt_rec(c,h,t) \\<in> C(t)";
+    (*instead of induct_tac "t", since t \\<in> bt(A) isn't an assumption*)
 by (rtac (major RS bt.induct) 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
 qed "bt_rec_type";
 
 (** n_nodes **)
 
-Goal "t: bt(A) ==> n_nodes(t) : nat";
+Goal "t \\<in> bt(A) ==> n_nodes(t) \\<in> nat";
 by (induct_tac "t" 1);
 by Auto_tac;
 qed "n_nodes_type";
@@ -59,14 +59,14 @@
 
 (** n_leaves **)
 
-Goal "t: bt(A) ==> n_leaves(t) : nat";
+Goal "t \\<in> bt(A) ==> n_leaves(t) \\<in> nat";
 by (induct_tac "t" 1);
 by Auto_tac;
 qed "n_leaves_type";
 
 (** bt_reflect **)
 
-Goal "t: bt(A) ==> bt_reflect(t) : bt(A)";
+Goal "t \\<in> bt(A) ==> bt_reflect(t) \\<in> bt(A)";
 by (induct_tac "t" 1);
 by Auto_tac;
 qed "bt_reflect_type";
@@ -80,19 +80,19 @@
 
 (*** theorems about n_leaves ***)
 
-Goal "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
+Goal "t \\<in> bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
 by (induct_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute, n_leaves_type])));
 qed "n_leaves_reflect";
 
-Goal "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
+Goal "t \\<in> bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
 by (induct_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_succ_right])));
 qed "n_leaves_nodes";
 
 (*** theorems about bt_reflect ***)
 
-Goal "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
+Goal "t \\<in> bt(A) ==> bt_reflect(bt_reflect(t))=t";
 by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "bt_reflect_bt_reflect_ident";

--- a/src/ZF/ex/BT.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/BT.thy	Mon May 21 14:36:24 2001 +0200
@@ -11,7 +11,7 @@
     bt          :: i=>i
 
 datatype
-  "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
+  "bt(A)" = Lf  |  Br ("a \\<in> A",  "t1: bt(A)",  "t2: bt(A)")
 
 consts
     n_nodes     :: i=>i

--- a/src/ZF/ex/Brouwer.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Brouwer.ML	Mon May 21 14:36:24 2001 +0200
@@ -20,10 +20,10 @@
 
 (*A nicer induction rule than the standard one*)
 val major::prems = goal Brouwer.thy
-    "[| b: brouwer;                                     \
+    "[| b \\<in> brouwer;                                     \
 \       P(Zero);                                        \
-\       !!b. [| b: brouwer;  P(b) |] ==> P(Suc(b));     \
-\       !!h. [| h: nat -> brouwer;  ALL i:nat. P(h`i)   \
+\       !!b. [| b \\<in> brouwer;  P(b) |] ==> P(Suc(b));     \
+\       !!h. [| h \\<in> nat -> brouwer;  \\<forall>i \\<in> nat. P(h`i)   \
 \            |] ==> P(Lim(h))                           \
 \    |] ==> P(b)";
 by (rtac (major RS brouwer.induct) 1);
@@ -35,7 +35,7 @@
 
 (** The Martin-L�f wellordering type **)
 
-Goal "Well(A,B) = (SUM x:A. B(x) -> Well(A,B))";
+Goal "Well(A,B) = (\\<Sigma>x \\<in> A. B(x) -> Well(A,B))";
 let open Well;  val rew = rewrite_rule con_defs in  
 by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
@@ -43,8 +43,8 @@
 
 (*A nicer induction rule than the standard one*)
 val major::prems = goal Brouwer.thy
-    "[| w: Well(A,B);                                                   \
-\       !!a f. [| a: A;  f: B(a) -> Well(A,B);  ALL y: B(a). P(f`y)     \
+    "[| w \\<in> Well(A,B);                                                   \
+\       !!a f. [| a \\<in> A;  f \\<in> B(a) -> Well(A,B);  \\<forall>y \\<in> B(a). P(f`y)     \
 \            |] ==> P(Sup(a,f))                                         \
 \    |] ==> P(w)";
 by (rtac (major RS Well.induct) 1);

--- a/src/ZF/ex/Brouwer.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Brouwer.thy	Mon May 21 14:36:24 2001 +0200
@@ -14,13 +14,13 @@
   Well    :: [i,i=>i]=>i
  
 datatype <= "Vfrom(0, csucc(nat))"
-  "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
+  "brouwer" = Zero | Suc ("b \\<in> brouwer") | Lim ("h \\<in> nat -> brouwer")
   monos        Pi_mono
   type_intrs  "inf_datatype_intrs"
 
 (*The union with nat ensures that the cardinal is infinite*)
-datatype <= "Vfrom(A Un (UN x:A. B(x)), csucc(nat Un |UN x:A. B(x)|))"
-  "Well(A,B)" = Sup ("a:A", "f: B(a) -> Well(A,B)")
+datatype <= "Vfrom(A Un (\\<Union>x \\<in> A. B(x)), csucc(nat Un |\\<Union>x \\<in> A. B(x)|))"
+  "Well(A,B)" = Sup ("a \\<in> A", "f \\<in> B(a) -> Well(A,B)")
   monos        Pi_mono
   type_intrs  "[[UN_upper_cardinal, le_nat_Un_cardinal] MRS le_trans]   
                @ inf_datatype_intrs"

--- a/src/ZF/ex/CoUnit.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/CoUnit.ML	Mon May 21 14:36:24 2001 +0200
@@ -11,7 +11,7 @@
 *)
 
 (*USELESS because folding on Con(?xa) == ?xa fails*)
-val ConE = counit.mk_cases "Con(x) : counit";
+val ConE = counit.mk_cases "Con(x) \\<in> counit";
 
 (*Proving freeness results*)
 val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y";
@@ -31,7 +31,7 @@
   The resulting set is a singleton.
 *)
 
-val Con2E = counit2.mk_cases "Con2(x,y) : counit2";
+val Con2E = counit2.mk_cases "Con2(x,y) \\<in> counit2";
 
 (*Proving freeness results*)
 val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
@@ -41,7 +41,7 @@
 by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
 qed "Con2_bnd_mono";
 
-Goal "lfp(univ(0), %x. Con2(x,x)) : counit2";
+Goal "lfp(univ(0), %x. Con2(x,x)) \\<in> counit2";
 by (rtac (singletonI RS counit2.coinduct) 1);
 by (rtac (qunivI RS singleton_subsetI) 1);
 by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
@@ -49,7 +49,7 @@
 qed "lfp_Con2_in_counit2";
 
 (*Lemma for proving finality.  Borrowed from ex/llist_eq.ML!*)
-Goal "Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y";
+Goal "Ord(i) ==> \\<forall>x y. x \\<in> counit2 & y \\<in> counit2 --> x Int Vset(i) \\<subseteq> y";
 by (etac trans_induct 1);
 by (safe_tac subset_cs);
 by (etac counit2.elim 1);
@@ -63,7 +63,7 @@
 val counit2_Int_Vset_subset = standard
         (counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
 
-Goal "[| x: counit2;  y: counit2 |] ==> x=y";
+Goal "[| x \\<in> counit2;  y \\<in> counit2 |] ==> x=y";
 by (rtac equalityI 1);
 by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
 qed "counit2_implies_equal";

--- a/src/ZF/ex/CoUnit.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/CoUnit.thy	Mon May 21 14:36:24 2001 +0200
@@ -19,7 +19,7 @@
 consts
   counit :: i
 codatatype
-  "counit" = Con ("x: counit")
+  "counit" = Con ("x \\<in> counit")
 
 
 (*A similar example, but the constructor is non-degenerate and it works!
@@ -29,6 +29,6 @@
 consts
   counit2 :: i
 codatatype
-  "counit2" = Con2 ("x: counit2", "y: counit2")
+  "counit2" = Con2 ("x \\<in> counit2", "y \\<in> counit2")
 
 end

--- a/src/ZF/ex/Comb.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Comb.ML	Mon May 21 14:36:24 2001 +0200
@@ -19,7 +19,7 @@
 
 Goalw [diamond_def]
     "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
-\    ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
+\    \\<forall>y'. <x,y'>:r --> (\\<exists>z. <y',z>: r^+ & <y,z>: r)";
 by (etac trancl_induct 1);
 by (blast_tac (claset() addIs [r_into_trancl]) 1);
 by (slow_best_tac (claset() addSDs [spec RS mp]
@@ -37,14 +37,14 @@
 
 
 val [_,_,comb_Ap] = comb.intrs;
-val Ap_E = comb.mk_cases "p#q : comb";
+val Ap_E = comb.mk_cases "p#q \\<in> comb";
 
 AddSIs comb.intrs;
 
 
 (*** Results about Contraction ***)
 
-(*For type checking: replaces a-1->b by a,b:comb *)
+(*For type checking: replaces a-1->b by a,b \\<in> comb *)
 val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
 val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1;
 val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
@@ -67,11 +67,11 @@
                      contract.Ap2 RS rtrancl_into_rtrancl2];
 
 (*Example only: not used*)
-Goalw [I_def] "p:comb ==> I#p ---> p";
+Goalw [I_def] "p \\<in> comb ==> I#p ---> p";
 by (blast_tac (claset() addIs reduction_rls) 1);
 qed "reduce_I";
 
-Goalw [I_def] "I: comb";
+Goalw [I_def] "I \\<in> comb";
 by (Blast_tac 1);
 qed "comb_I";
 
@@ -89,11 +89,11 @@
 by Auto_tac;
 qed "I_contract_E";
 
-Goal "K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
+Goal "K#p -1-> r ==> (\\<exists>q. r = K#q & p -1-> q)";
 by Auto_tac;
 qed "K1_contractD";
 
-Goal "[| p ---> q;  r: comb |] ==> p#r ---> q#r";
+Goal "[| p ---> q;  r \\<in> comb |] ==> p#r ---> q#r";
 by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
 by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
 by (etac rtrancl_induct 1);
@@ -102,7 +102,7 @@
 by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1);
 qed "Ap_reduce1";
 
-Goal "[| p ---> q;  r: comb |] ==> r#p ---> r#q";
+Goal "[| p ---> q;  r \\<in> comb |] ==> r#p ---> r#q";
 by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
 by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
 by (etac rtrancl_induct 1);
@@ -134,7 +134,7 @@
 
 (*** Results about Parallel Contraction ***)
 
-(*For type checking: replaces a=1=>b by a,b:comb *)
+(*For type checking: replaces a=1=>b by a,b \\<in> comb *)
 val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
 val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1;
 val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
@@ -154,17 +154,17 @@
 
 (*** Basic properties of parallel contraction ***)
 
-Goal "K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
+Goal "K#p =1=> r ==> (\\<exists>p'. r = K#p' & p =1=> p')";
 by Auto_tac;
 qed "K1_parcontractD";
 AddSDs [K1_parcontractD];
 
-Goal "S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
+Goal "S#p =1=> r ==> (\\<exists>p'. r = S#p' & p =1=> p')";
 by Auto_tac;
 qed "S1_parcontractD";
 AddSDs [S1_parcontractD];
 
-Goal "S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
+Goal "S#p#q =1=> r ==> (\\<exists>p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
 by Auto_tac;
 qed "S2_parcontractD";
 AddSDs [S2_parcontractD];

--- a/src/ZF/ex/Comb.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Comb.thy	Mon May 21 14:36:24 2001 +0200
@@ -20,7 +20,7 @@
 datatype
   "comb" = K
          | S
-         | "#" ("p: comb", "q: comb")   (infixl 90)
+         | "#" ("p \\<in> comb", "q \\<in> comb")   (infixl 90)
 
 (** Inductive definition of contractions, -1->
              and (multi-step) reductions, --->
@@ -31,16 +31,16 @@
   "--->"    :: [i,i] => o                       (infixl 50)
 
 translations
-  "p -1-> q" == "<p,q> : contract"
-  "p ---> q" == "<p,q> : contract^*"
+  "p -1-> q" == "<p,q> \\<in> contract"
+  "p ---> q" == "<p,q> \\<in> contract^*"
 
 inductive
   domains   "contract" <= "comb*comb"
   intrs
-    K     "[| p:comb;  q:comb |] ==> K#p#q -1-> p"
-    S     "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
-    Ap1   "[| p-1->q;  r:comb |] ==> p#r -1-> q#r"
-    Ap2   "[| p-1->q;  r:comb |] ==> r#p -1-> r#q"
+    K     "[| p \\<in> comb;  q \\<in> comb |] ==> K#p#q -1-> p"
+    S     "[| p \\<in> comb;  q \\<in> comb;  r \\<in> comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
+    Ap1   "[| p-1->q;  r \\<in> comb |] ==> p#r -1-> q#r"
+    Ap2   "[| p-1->q;  r \\<in> comb |] ==> r#p -1-> r#q"
   type_intrs "comb.intrs"
 
 
@@ -53,15 +53,15 @@
   "===>"    :: [i,i] => o                       (infixl 50)
 
 translations
-  "p =1=> q" == "<p,q> : parcontract"
-  "p ===> q" == "<p,q> : parcontract^+"
+  "p =1=> q" == "<p,q> \\<in> parcontract"
+  "p ===> q" == "<p,q> \\<in> parcontract^+"
 
 inductive
   domains   "parcontract" <= "comb*comb"
   intrs
-    refl  "[| p:comb |] ==> p =1=> p"
-    K     "[| p:comb;  q:comb |] ==> K#p#q =1=> p"
-    S     "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
+    refl  "[| p \\<in> comb |] ==> p =1=> p"
+    K     "[| p \\<in> comb;  q \\<in> comb |] ==> K#p#q =1=> p"
+    S     "[| p \\<in> comb;  q \\<in> comb;  r \\<in> comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
     Ap    "[| p=1=>q;  r=1=>s |] ==> p#r =1=> q#s"
   type_intrs "comb.intrs"
 
@@ -72,8 +72,8 @@
   "I == S#K#K"
 
   diamond :: i => o
-  "diamond(r) == ALL x y. <x,y>:r --> 
-                          (ALL y'. <x,y'>:r --> 
-                                   (EX z. <y,z>:r & <y',z> : r))"
+  "diamond(r) == \\<forall>x y. <x,y>:r --> 
+                          (\\<forall>y'. <x,y'>:r --> 
+                                   (\\<exists>z. <y,z>:r & <y',z> \\<in> r))"
 
 end

--- a/src/ZF/ex/Commutation.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Commutation.ML	Mon May 21 14:36:24 2001 +0200
@@ -12,7 +12,7 @@
 qed "square_sym";                
 
 
-Goalw [square_def] "[| square(r,s,t,u); t <= t' |] ==> square(r,s,t',u)";
+Goalw [square_def] "[| square(r,s,t,u); t \\<subseteq> t' |] ==> square(r,s,t',u)";
 by (Blast_tac 1);
 qed "square_subset"; 
 
@@ -81,7 +81,7 @@
 
 Goalw [confluent_def]
  "[| confluent(r); confluent(s); commute(r^*, s^*); \
-\           r<=Sigma(A,B); s<=Sigma(C,D) |] ==> confluent(r Un s)";
+\           r \\<subseteq> Sigma(A,B); s \\<subseteq> Sigma(C,D) |] ==> confluent(r Un s)";
 by (rtac (rtrancl_Un_rtrancl RS subst) 1);
 by (blast_tac (claset() addDs [diamond_Un] 
      addIs [rewrite_rule [confluent_def] diamond_confluent]) 3);
@@ -90,7 +90,7 @@
 
 
 Goal
- "[| diamond(r); s<=r; r<= s^* |] ==> confluent(s)";
+ "[| diamond(r); s \\<subseteq> r; r<= s^* |] ==> confluent(s)";
 by (dresolve_tac [rtrancl_subset RS sym] 1);
 by (assume_tac 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def])));

--- a/src/ZF/ex/Commutation.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Commutation.thy	Mon May 21 14:36:24 2001 +0200
@@ -12,8 +12,8 @@
 constdefs
   square  :: [i, i, i, i] => o
    "square(r,s,t,u) ==
-   (ALL a b. <a,b>:r --> (ALL c. <a, c>:s
-                          --> (EX x. <b,x>:t & <c,x>:u)))"
+   (\\<forall>a b. <a,b>:r --> (\\<forall>c. <a, c>:s
+                          --> (\\<exists>x. <b,x>:t & <c,x>:u)))"
 
    commute :: [i, i] => o       
    "commute(r,s) == square(r,s,s,r)"
@@ -25,8 +25,8 @@
   "strip(r) == commute(r^*, r)"
 
   Church_Rosser :: i => o     
-  "Church_Rosser(r) == (ALL x y. <x,y>: (r Un converse(r))^* -->
-			(EX z. <x,z>:r^* & <y,z>:r^*))"
+  "Church_Rosser(r) == (\\<forall>x y. <x,y>: (r Un converse(r))^* -->
+			(\\<exists>z. <x,z>:r^* & <y,z>:r^*))"
   confluent :: i=>o    
   "confluent(r) == diamond(r^*)"
 end

--- a/src/ZF/ex/Data.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Data.ML	Mon May 21 14:36:24 2001 +0200
@@ -17,13 +17,13 @@
 
 (**  Lemmas to justify using "data" in other recursive type definitions **)
 
-Goalw data.defs "[| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
+Goalw data.defs "[| A \\<subseteq> C; B \\<subseteq> D |] ==> data(A,B) \\<subseteq> data(C,D)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac data.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
 qed "data_mono";
 
-Goalw (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
+Goalw (data.defs@data.con_defs) "data(univ(A),univ(A)) \\<subseteq> univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
 by (fast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,

--- a/src/ZF/ex/Data.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Data.thy	Mon May 21 14:36:24 2001 +0200
@@ -14,8 +14,8 @@
 
 datatype
   "data(A,B)" = Con0
-              | Con1 ("a: A")
-              | Con2 ("a: A", "b: B")
-              | Con3 ("a: A", "b: B", "d: data(A,B)")
+              | Con1 ("a \\<in> A")
+              | Con2 ("a \\<in> A", "b \\<in> B")
+              | Con3 ("a \\<in> A", "b \\<in> B", "d \\<in> data(A,B)")
 
 end

--- a/src/ZF/ex/Enum.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Enum.ML	Mon May 21 14:36:24 2001 +0200
@@ -8,7 +8,7 @@
 Can go up to at least 100 constructors, but it takes nearly 7 minutes...
 *)
 
-Goal "C00 ~= C01";
+Goal "C00 \\<noteq> C01";
 by (Simp_tac 1);
 result();

--- a/src/ZF/ex/LList.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/LList.ML	Mon May 21 14:36:24 2001 +0200
@@ -16,7 +16,7 @@
 	Un_upper1, Un_upper2, Int_lower1, Int_lower2];
 
 (*An elimination rule, for type-checking*)
-val LConsE = llist.mk_cases "LCons(a,l) : llist(A)";
+val LConsE = llist.mk_cases "LCons(a,l) \\<in> llist(A)";
 
 (*Proving freeness results*)
 val LCons_iff      = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
@@ -30,7 +30,7 @@
 
 (*** Lemmas to justify using "llist" in other recursive type definitions ***)
 
-Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
+Goalw llist.defs "A \\<subseteq> B ==> llist(A) \\<subseteq> llist(B)";
 by (rtac gfp_mono 1);
 by (REPEAT (rtac llist.bnd_mono 1));
 by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
@@ -44,7 +44,7 @@
 AddSDs [qunivD];
 AddSEs [Ord_in_Ord];
 
-Goal "Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
+Goal "Ord(i) ==> \\<forall>l \\<in> llist(quniv(A)). l Int Vset(i) \\<subseteq> univ(eclose(A))";
 by (etac trans_induct 1);
 by (rtac ballI 1);
 by (etac llist.elim 1);
@@ -55,7 +55,7 @@
 by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
 qed "llist_quniv_lemma";
 
-Goal "llist(quniv(A)) <= quniv(A)";
+Goal "llist(quniv(A)) \\<subseteq> quniv(A)";
 by (rtac (qunivI RS subsetI) 1);
 by (rtac Int_Vset_subset 1);
 by (REPEAT (ares_tac [llist_quniv_lemma RS bspec] 1));
@@ -71,7 +71,7 @@
 AddSEs [Ord_in_Ord, Pair_inject];
 
 (*Lemma for proving finality.  Unfold the lazy list; use induction hypothesis*)
-Goal "Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
+Goal "Ord(i) ==> \\<forall>l l'. <l,l'> \\<in> lleq(A) --> l Int Vset(i) \\<subseteq> l'";
 by (etac trans_induct 1);
 by (REPEAT (resolve_tac [allI, impI] 1));
 by (etac lleq.elim 1);
@@ -85,7 +85,7 @@
 
 
 (*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
-val [prem] = goal LList.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
+val [prem] = goal LList.thy "<l,l'> \\<in> lleq(A) ==> <l',l> \\<in> lleq(A)";
 by (rtac (prem RS converseI RS lleq.coinduct) 1);
 by (rtac (lleq.dom_subset RS converse_type) 1);
 by Safe_tac;
@@ -93,15 +93,15 @@
 by (ALLGOALS Fast_tac);
 qed "lleq_symmetric";
 
-Goal "<l,l'> : lleq(A) ==> l=l'";
+Goal "<l,l'> \\<in> lleq(A) ==> l=l'";
 by (rtac equalityI 1);
 by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
      ORELSE etac lleq_symmetric 1));
 qed "lleq_implies_equal";
 
 val [eqprem,lprem] = goal LList.thy
-    "[| l=l';  l: llist(A) |] ==> <l,l'> : lleq(A)";
-by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] lleq.coinduct 1);
+    "[| l=l';  l \\<in> llist(A) |] ==> <l,l'> \\<in> lleq(A)";
+by (res_inst_tac [("X", "{<l,l>. l \\<in> llist(A)}")] lleq.coinduct 1);
 by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
 by Safe_tac;
 by (etac llist.elim 1);
@@ -130,12 +130,12 @@
 
 bind_thm ("member_subset_Union_eclose", (arg_into_eclose RS Union_upper));
 
-Goal "a : A ==> lconst(a) : quniv(A)";
+Goal "a \\<in> A ==> lconst(a) \\<in> quniv(A)";
 by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
 by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
 qed "lconst_in_quniv";
 
-Goal "a:A ==> lconst(a): llist(A)";
+Goal "a \\<in> A ==> lconst(a): llist(A)";
 by (rtac (singletonI RS llist.coinduct) 1);
 by (etac (lconst_in_quniv RS singleton_subsetI) 1);
 by (fast_tac (claset() addSIs [lconst]) 1);
@@ -145,7 +145,7 @@
 
 Addsimps [flip_LNil, flip_LCons, not_type];
 
-goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
+goal QUniv.thy "!!b. b \\<in> bool ==> b Int X \\<subseteq> univ(eclose(A))";
 by (fast_tac (claset() addIs [Int_lower1 RS subset_trans] addSEs [boolE]) 1);
 qed "bool_Int_subset_univ";
 
@@ -154,7 +154,7 @@
 
 (*Reasoning borrowed from lleq.ML; a similar proof works for all
   "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
-Goal "Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
+Goal "Ord(i) ==> \\<forall>l \\<in> llist(bool). flip(l) Int Vset(i) \\<subseteq> \
 \                   univ(eclose(bool))";
 by (etac trans_induct 1);
 by (rtac ballI 1);
@@ -166,13 +166,13 @@
 by (deepen_tac (claset() addIs [Ord_trans, Int_lower1 RS subset_trans]) 2 1);
 qed "flip_llist_quniv_lemma";
 
-Goal "l: llist(bool) ==> flip(l) : quniv(bool)";
+Goal "l \\<in> llist(bool) ==> flip(l) \\<in> quniv(bool)";
 by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
 by (REPEAT (assume_tac 1));
 qed "flip_in_quniv";
 
-val [prem] = goal LList.thy "l : llist(bool) ==> flip(l): llist(bool)";
-by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
+val [prem] = goal LList.thy "l \\<in> llist(bool) ==> flip(l): llist(bool)";
+by (res_inst_tac [("X", "{flip(l) . l \\<in> llist(bool)}")]
        llist.coinduct 1);
 by (rtac (prem RS RepFunI) 1);
 by (fast_tac (claset() addSIs [flip_in_quniv]) 1);
@@ -183,8 +183,8 @@
 qed "flip_type";
 
 val [prem] = goal LList.thy
-    "l : llist(bool) ==> flip(flip(l)) = l";
-by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
+    "l \\<in> llist(bool) ==> flip(flip(l)) = l";
+by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l \\<in> llist(bool)}")]
        (lleq.coinduct RS lleq_implies_equal) 1);
 by (rtac (prem RS RepFunI) 1);
 by (fast_tac (claset() addSIs [flip_type]) 1);

--- a/src/ZF/ex/LList.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/LList.thy	Mon May 21 14:36:24 2001 +0200
@@ -20,7 +20,7 @@
   llist  :: i=>i
 
 codatatype
-  "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
+  "llist(A)" = LNil | LCons ("a \\<in> A", "l \\<in> llist(A)")
 
 
 (*Coinductive definition of equality*)
@@ -33,8 +33,8 @@
 coinductive
   domains "lleq(A)" <= "llist(A) * llist(A)"
   intrs
-    LNil  "<LNil, LNil> : lleq(A)"
-    LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
+    LNil  "<LNil, LNil> \\<in> lleq(A)"
+    LCons "[| a \\<in> A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
   type_intrs  "llist.intrs"
 
 
@@ -49,7 +49,7 @@
 rules
   flip_LNil   "flip(LNil) = LNil"
 
-  flip_LCons  "[| x:bool; l: llist(bool) |] ==> 
+  flip_LCons  "[| x \\<in> bool; l \\<in> llist(bool) |] ==> 
               flip(LCons(x,l)) = LCons(not(x), flip(l))"
 
 end

--- a/src/ZF/ex/Limit.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Limit.ML	Mon May 21 14:36:24 2001 +0200
@@ -19,7 +19,7 @@
 (* Basic results.                                                       *)
 (*----------------------------------------------------------------------*)
 
-Goalw [set_def] "x:fst(D) ==> x:set(D)";
+Goalw [set_def] "x \\<in> fst(D) ==> x \\<in> set(D)";
 by (assume_tac 1);
 qed "set_I";
 
@@ -35,25 +35,25 @@
 (* I/E/D rules for po and cpo.                                          *)
 (*----------------------------------------------------------------------*)
 
-Goalw [po_def] "[|po(D); x:set(D)|] ==> rel(D,x,x)";
+Goalw [po_def] "[|po(D); x \\<in> set(D)|] ==> rel(D,x,x)";
 by (Blast_tac 1);
 qed "po_refl";
 
-Goalw [po_def] "[|po(D); rel(D,x,y); rel(D,y,z); x:set(D);  \
-\                 y:set(D); z:set(D)|] ==> rel(D,x,z)";
+Goalw [po_def] "[|po(D); rel(D,x,y); rel(D,y,z); x \\<in> set(D);  \
+\                 y \\<in> set(D); z \\<in> set(D)|] ==> rel(D,x,z)";
 by (Blast_tac 1);
 qed "po_trans";
 
 Goalw [po_def]
-    "[|po(D); rel(D,x,y); rel(D,y,x); x:set(D); y:set(D)|] ==> x = y";
+    "[|po(D); rel(D,x,y); rel(D,y,x); x \\<in> set(D); y \\<in> set(D)|] ==> x = y";
 by (Blast_tac 1);
 qed "po_antisym";
 
 val prems = Goalw [po_def]
-    "[| !!x. x:set(D) ==> rel(D,x,x);   \
-\       !!x y z. [| rel(D,x,y); rel(D,y,z); x:set(D); y:set(D); z:set(D)|] ==> \
+    "[| !!x. x \\<in> set(D) ==> rel(D,x,x);   \
+\       !!x y z. [| rel(D,x,y); rel(D,y,z); x \\<in> set(D); y \\<in> set(D); z \\<in> set(D)|] ==> \
 \                rel(D,x,z);  \
-\       !!x y. [| rel(D,x,y); rel(D,y,x); x:set(D); y:set(D)|] ==> x=y |] ==> \
+\       !!x y. [| rel(D,x,y); rel(D,y,x); x \\<in> set(D); y \\<in> set(D)|] ==> x=y |] ==> \
 \    po(D)";
 by (blast_tac (claset() addIs prems) 1);
 qed "poI";
@@ -67,7 +67,7 @@
 by (Blast_tac 1);
 qed "cpo_po";
 
-Goal "[|cpo(D); x:set(D)|] ==> rel(D,x,x)";
+Goal "[|cpo(D); x \\<in> set(D)|] ==> rel(D,x,x)";
 by (blast_tac (claset() addIs [po_refl, cpo_po]) 1);
 qed "cpo_refl";
 
@@ -75,12 +75,12 @@
 AddSIs   [cpo_refl];
 AddTCs   [cpo_refl];
 
-Goal "[|cpo(D); rel(D,x,y); rel(D,y,z); x:set(D);  \
-\       y:set(D); z:set(D)|] ==> rel(D,x,z)";
+Goal "[|cpo(D); rel(D,x,y); rel(D,y,z); x \\<in> set(D);  \
+\       y \\<in> set(D); z \\<in> set(D)|] ==> rel(D,x,z)";
 by (blast_tac (claset() addIs [cpo_po, po_trans]) 1);
 qed "cpo_trans";
 
-Goal "[|cpo(D); rel(D,x,y); rel(D,y,x); x:set(D); y:set(D)|] ==> x = y";
+Goal "[|cpo(D); rel(D,x,y); rel(D,y,x); x \\<in> set(D); y \\<in> set(D)|] ==> x = y";
 by (blast_tac (claset() addIs [cpo_po, po_antisym]) 1);
 qed "cpo_antisym";
 
@@ -98,11 +98,11 @@
 by (Asm_simp_tac 1);
 qed "islub_isub";
 
-Goalw [islub_def,isub_def] "islub(D,X,x) ==> x:set(D)";
+Goalw [islub_def,isub_def] "islub(D,X,x) ==> x \\<in> set(D)";
 by (Asm_simp_tac 1);
 qed "islub_in";
 
-Goalw [islub_def,isub_def] "[|islub(D,X,x); n:nat|] ==> rel(D,X`n,x)";
+Goalw [islub_def,isub_def] "[|islub(D,X,x); n \\<in> nat|] ==> rel(D,X`n,x)";
 by (Asm_simp_tac 1);
 qed "islub_ub";
 
@@ -116,21 +116,21 @@
 qed "islubI";
 
 val prems = Goalw [isub_def]  (* isubI *)
-    "[|x:set(D);  !!n. n:nat ==> rel(D,X`n,x)|] ==> isub(D,X,x)";
+    "[|x \\<in> set(D);  !!n. n \\<in> nat ==> rel(D,X`n,x)|] ==> isub(D,X,x)";
 by (blast_tac (claset() addIs prems) 1);
 qed "isubI";
 
 val prems = Goalw [isub_def]  (* isubE *)
-    "[|isub(D,X,x); [|x:set(D);  !!n. n:nat==>rel(D,X`n,x)|] ==> P \
+    "[|isub(D,X,x); [|x \\<in> set(D);  !!n. n \\<in> nat==>rel(D,X`n,x)|] ==> P \
 \    |] ==> P";
 by (asm_simp_tac (simpset() addsimps prems) 1);
 qed "isubE";
 
-Goalw [isub_def] "isub(D,X,x) ==> x:set(D)";
+Goalw [isub_def] "isub(D,X,x) ==> x \\<in> set(D)";
 by (Asm_simp_tac 1);
 qed "isubD1";
 
-Goalw [isub_def] "[|isub(D,X,x); n:nat|]==>rel(D,X`n,x)";
+Goalw [isub_def] "[|isub(D,X,x); n \\<in> nat|]==>rel(D,X`n,x)";
 by (Asm_simp_tac 1);
 qed "isubD2";
 
@@ -152,32 +152,32 @@
 (*----------------------------------------------------------------------*)
 
 val prems = Goalw [chain_def]
- "[|X:nat->set(D);  !!n. n:nat ==> rel(D,X`n,X`succ(n))|] ==> chain(D,X)";
+ "[|X \\<in> nat->set(D);  !!n. n \\<in> nat ==> rel(D,X`n,X`succ(n))|] ==> chain(D,X)";
 by (blast_tac (claset() addIs prems) 1);
 qed "chainI";
 
-Goalw [chain_def] "chain(D,X) ==> X : nat -> set(D)";
+Goalw [chain_def] "chain(D,X) ==> X \\<in> nat -> set(D)";
 by (Asm_simp_tac 1);
 qed "chain_fun";
 
-Goalw [chain_def] "[|chain(D,X); n:nat|] ==> X`n : set(D)";
+Goalw [chain_def] "[|chain(D,X); n \\<in> nat|] ==> X`n \\<in> set(D)";
 by (blast_tac (claset() addDs [apply_type]) 1);
 qed "chain_in";
 
-Goalw [chain_def] "[|chain(D,X); n:nat|] ==> rel(D, X ` n, X ` succ(n))";
+Goalw [chain_def] "[|chain(D,X); n \\<in> nat|] ==> rel(D, X ` n, X ` succ(n))";
 by (Blast_tac 1);
 qed "chain_rel";
 
 Addsimps [chain_in, chain_rel];
 AddTCs   [chain_fun, chain_in, chain_rel];
 
-Goal "[|chain(D,X); cpo(D); n:nat; m:nat|] ==> rel(D,X`n,(X`(m #+ n)))";
+Goal "[|chain(D,X); cpo(D); n \\<in> nat; m \\<in> nat|] ==> rel(D,X`n,(X`(m #+ n)))";
 by (induct_tac "m" 1);
 by (auto_tac (claset() addIs [cpo_trans], simpset()));  
 qed "chain_rel_gen_add";
 
 Goal  (* chain_rel_gen *)
-    "[|n le m; chain(D,X); cpo(D); m:nat|] ==> rel(D,X`n,X`m)";
+    "[|n le m; chain(D,X); cpo(D); m \\<in> nat|] ==> rel(D,X`n,X`m)";
 by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
 by (etac rev_mp 1);  (*prepare the induction*)
 by (induct_tac "m" 1);
@@ -190,7 +190,7 @@
 (*----------------------------------------------------------------------*)
 
 val prems = Goalw [pcpo_def]  (* pcpoI *)
-    "[|!!y. y:set(D)==>rel(D,x,y); x:set(D); cpo(D)|]==>pcpo(D)";
+    "[|!!y. y \\<in> set(D)==>rel(D,x,y); x \\<in> set(D); cpo(D)|]==>pcpo(D)";
 by (auto_tac (claset() addIs prems, simpset()));
 qed "pcpoI";
 
@@ -199,12 +199,12 @@
 qed "pcpo_cpo";
 
 Goalw [pcpo_def] (* pcpo_bot_ex1 *)
-    "pcpo(D) ==> EX! x. x:set(D) & (ALL y:set(D). rel(D,x,y))";
+    "pcpo(D) ==> \\<exists>! x. x \\<in> set(D) & (\\<forall>y \\<in> set(D). rel(D,x,y))";
 by (blast_tac (claset() addIs [cpo_antisym]) 1);
 qed "pcpo_bot_ex1";
 
 Goalw [bot_def] (* bot_least *)
-    "[| pcpo(D); y:set(D)|] ==> rel(D,bot(D),y)";
+    "[| pcpo(D); y \\<in> set(D)|] ==> rel(D,bot(D),y)";
 by (best_tac (claset() addIs [pcpo_bot_ex1 RS theI2]) 1);
 qed "bot_least";
 
@@ -216,7 +216,7 @@
 AddTCs [pcpo_cpo, bot_least, bot_in];
 
 val prems = Goal  (* bot_unique *)
-    "[| pcpo(D); x:set(D); !!y. y:set(D) ==> rel(D,x,y)|] ==> x = bot(D)";
+    "[| pcpo(D); x \\<in> set(D); !!y. y \\<in> set(D) ==> rel(D,x,y)|] ==> x = bot(D)";
 by (blast_tac (claset() addIs ([cpo_antisym,pcpo_cpo,bot_in,bot_least]@
                                prems)) 1);
 qed "bot_unique";
@@ -225,17 +225,17 @@
 (* Constant chains and lubs and cpos.                                   *)
 (*----------------------------------------------------------------------*)
 
-Goalw [chain_def] "[|x:set(D); cpo(D)|] ==> chain(D,(lam n:nat. x))";
+Goalw [chain_def] "[|x \\<in> set(D); cpo(D)|] ==> chain(D,(\\<lambda>n \\<in> nat. x))";
 by (asm_simp_tac (simpset() addsimps [lam_type, nat_succI]) 1);
 qed "chain_const";
 
 Goalw [islub_def,isub_def] 
-   "[|x:set(D); cpo(D)|] ==> islub(D,(lam n:nat. x),x)";
+   "[|x \\<in> set(D); cpo(D)|] ==> islub(D,(\\<lambda>n \\<in> nat. x),x)";
 by (Asm_simp_tac 1);
 by (Blast_tac 1);
 qed "islub_const";
 
-Goal "[|x:set(D); cpo(D)|] ==> lub(D,lam n:nat. x) = x";
+Goal "[|x \\<in> set(D); cpo(D)|] ==> lub(D,\\<lambda>n \\<in> nat. x) = x";
 by (blast_tac (claset() addIs [islub_unique, cpo_lub,
 			       chain_const, islub_const]) 1);
 qed "lub_const";
@@ -266,21 +266,21 @@
 (*----------------------------------------------------------------------*)
 
 val prems = Goalw [dominate_def]
-  "[| !!m. m:nat ==> n(m):nat; !!m. m:nat ==> rel(D,X`m,Y`n(m))|] ==>   \
+  "[| !!m. m \\<in> nat ==> n(m):nat; !!m. m \\<in> nat ==> rel(D,X`m,Y`n(m))|] ==>   \
 \  dominate(D,X,Y)";
 by (blast_tac (claset() addIs prems) 1);
 qed "dominateI"; 
 
 Goalw [isub_def, dominate_def]
   "[|dominate(D,X,Y); isub(D,Y,x); cpo(D);  \
-\    X:nat->set(D); Y:nat->set(D)|] ==> isub(D,X,x)";
+\    X \\<in> nat->set(D); Y \\<in> nat->set(D)|] ==> isub(D,X,x)";
 by (Asm_full_simp_tac 1);  
 by (blast_tac (claset() addIs [cpo_trans] addSIs [apply_funtype]) 1);
 qed "dominate_isub";
 
 Goalw [islub_def]
   "[|dominate(D,X,Y); islub(D,X,x); islub(D,Y,y); cpo(D);  \
-\    X:nat->set(D); Y:nat->set(D)|] ==> rel(D,x,y)";
+\    X \\<in> nat->set(D); Y \\<in> nat->set(D)|] ==> rel(D,x,y)";
 by (blast_tac (claset() addIs [dominate_isub]) 1);
 qed "dominate_islub";
 
@@ -290,7 +290,7 @@
 qed "subchain_isub";
 
 Goal "[|dominate(D,X,Y); subchain(Y,X); islub(D,X,x); islub(D,Y,y); cpo(D);  \
-\    X:nat->set(D); Y:nat->set(D)|] ==> x = y";
+\    X \\<in> nat->set(D); Y \\<in> nat->set(D)|] ==> x = y";
 by (blast_tac (claset() addIs [cpo_antisym, dominate_islub, islub_least,
 			       subchain_isub, islub_isub, islub_in]) 1);
 qed "dominate_islub_eq";
@@ -300,63 +300,63 @@
 (*----------------------------------------------------------------------*)
 
 Goalw [matrix_def]  (* matrix_fun *)
-    "matrix(D,M) ==> M : nat -> (nat -> set(D))";
+    "matrix(D,M) ==> M \\<in> nat -> (nat -> set(D))";
 by (Asm_simp_tac 1);
 qed "matrix_fun";
 
-Goal "[|matrix(D,M); n:nat|] ==> M`n : nat -> set(D)";
+Goal "[|matrix(D,M); n \\<in> nat|] ==> M`n \\<in> nat -> set(D)";
 by (blast_tac (claset() addIs [apply_funtype, matrix_fun]) 1);
 qed "matrix_in_fun";
 
-Goal "[|matrix(D,M); n:nat; m:nat|] ==> M`n`m : set(D)";
+Goal "[|matrix(D,M); n \\<in> nat; m \\<in> nat|] ==> M`n`m \\<in> set(D)";
 by (blast_tac (claset() addIs [apply_funtype, matrix_in_fun]) 1);
 qed "matrix_in";
 
 Goalw [matrix_def]  (* matrix_rel_1_0 *)
-    "[|matrix(D,M); n:nat; m:nat|] ==> rel(D,M`n`m,M`succ(n)`m)";
+    "[|matrix(D,M); n \\<in> nat; m \\<in> nat|] ==> rel(D,M`n`m,M`succ(n)`m)";
 by (Asm_simp_tac 1);
 qed "matrix_rel_1_0";
 
 Goalw [matrix_def]  (* matrix_rel_0_1 *)
-    "[|matrix(D,M); n:nat; m:nat|] ==> rel(D,M`n`m,M`n`succ(m))";
+    "[|matrix(D,M); n \\<in> nat; m \\<in> nat|] ==> rel(D,M`n`m,M`n`succ(m))";
 by (Asm_simp_tac 1);
 qed "matrix_rel_0_1";
 
 Goalw [matrix_def]  (* matrix_rel_1_1 *)
-    "[|matrix(D,M); n:nat; m:nat|] ==> rel(D,M`n`m,M`succ(n)`succ(m))";
+    "[|matrix(D,M); n \\<in> nat; m \\<in> nat|] ==> rel(D,M`n`m,M`succ(n)`succ(m))";
 by (Asm_simp_tac 1);
 qed "matrix_rel_1_1";
 
-Goal "f:X->Y->Z ==> (lam y:Y. lam x:X. f`x`y):Y->X->Z";
+Goal "f \\<in> X->Y->Z ==> (\\<lambda>y \\<in> Y. \\<lambda>x \\<in> X. f`x`y):Y->X->Z";
 by (blast_tac (claset() addIs [lam_type, apply_funtype]) 1);
 qed "fun_swap";
 
 Goalw [matrix_def]  (* matrix_sym_axis *)
-    "matrix(D,M) ==> matrix(D,lam m:nat. lam n:nat. M`n`m)";
+    "matrix(D,M) ==> matrix(D,\\<lambda>m \\<in> nat. \\<lambda>n \\<in> nat. M`n`m)";
 by (asm_simp_tac (simpset() addsimps [fun_swap]) 1);
 qed "matrix_sym_axis";
 
 Goalw [chain_def]  (* matrix_chain_diag *)
-    "matrix(D,M) ==> chain(D,lam n:nat. M`n`n)";
+    "matrix(D,M) ==> chain(D,\\<lambda>n \\<in> nat. M`n`n)";
 by (auto_tac (claset() addIs [lam_type, matrix_in, matrix_rel_1_1], 
               simpset()));
 qed "matrix_chain_diag";
 
 Goalw [chain_def]  (* matrix_chain_left *)
-    "[|matrix(D,M); n:nat|] ==> chain(D,M`n)";
+    "[|matrix(D,M); n \\<in> nat|] ==> chain(D,M`n)";
 by (auto_tac (claset() addIs [matrix_fun RS apply_type, matrix_in, 
                               matrix_rel_0_1],   simpset()));
 qed "matrix_chain_left";
 
 Goalw [chain_def]  (* matrix_chain_right *)
-    "[|matrix(D,M); m:nat|] ==> chain(D,lam n:nat. M`n`m)";
+    "[|matrix(D,M); m \\<in> nat|] ==> chain(D,\\<lambda>n \\<in> nat. M`n`m)";
 by (auto_tac (claset() addIs [lam_type,matrix_in,matrix_rel_1_0],
 	      simpset()));
 qed "matrix_chain_right";
 
 val xprem::yprem::prems = Goalw [matrix_def]  (* matrix_chainI *)
-    "[|!!x. x:nat==>chain(D,M`x);  !!y. y:nat==>chain(D,lam x:nat. M`x`y);   \
-\      M:nat->nat->set(D); cpo(D)|] ==> matrix(D,M)";
+    "[|!!x. x \\<in> nat==>chain(D,M`x);  !!y. y \\<in> nat==>chain(D,\\<lambda>x \\<in> nat. M`x`y);   \
+\      M \\<in> nat->nat->set(D); cpo(D)|] ==> matrix(D,M)";
 by Safe_tac;
 by (cut_inst_tac[("y1","m"),("n","n")] (yprem RS chain_rel) 2);
 by (Asm_full_simp_tac 4);
@@ -367,18 +367,18 @@
 		                  xprem::yprem::prems));
 qed "matrix_chainI";
 
-Goal "[|m : nat; rel(D, (lam n:nat. M`n`n)`m, y)|] ==> rel(D,M`m`m, y)";
+Goal "[|m \\<in> nat; rel(D, (\\<lambda>n \\<in> nat. M`n`n)`m, y)|] ==> rel(D,M`m`m, y)";
 by (Asm_full_simp_tac 1);
 qed "lemma";
 
-Goal "[|x:nat; m:nat; rel(D,(lam n:nat. M`n`m1)`x,(lam n:nat. M`n`m1)`m)|] \
+Goal "[|x \\<in> nat; m \\<in> nat; rel(D,(\\<lambda>n \\<in> nat. M`n`m1)`x,(\\<lambda>n \\<in> nat. M`n`m1)`m)|] \
 \     ==> rel(D,M`x`m1,M`m`m1)";
 by (Asm_full_simp_tac 1);
 qed "lemma2";
 
 Goalw [isub_def]  (* isub_lemma *)
-    "[|isub(D, lam n:nat. M`n`n, y); matrix(D,M); cpo(D)|] ==>  \
-\    isub(D, lam n:nat. lub(D,lam m:nat. M`n`m), y)";
+    "[|isub(D, \\<lambda>n \\<in> nat. M`n`n, y); matrix(D,M); cpo(D)|] ==>  \
+\    isub(D, \\<lambda>n \\<in> nat. lub(D,\\<lambda>m \\<in> nat. M`n`m), y)";
 by Safe_tac;
 by (Asm_simp_tac 1);
 by (forward_tac [matrix_fun RS apply_type] 1);
@@ -407,7 +407,7 @@
 qed "isub_lemma";
 
 Goalw [chain_def]  (* matrix_chain_lub *)
-    "[|matrix(D,M); cpo(D)|] ==> chain(D,lam n:nat. lub(D,lam m:nat. M`n`m))";
+    "[|matrix(D,M); cpo(D)|] ==> chain(D,\\<lambda>n \\<in> nat. lub(D,\\<lambda>m \\<in> nat. M`n`m))";
 by Safe_tac;
 by (rtac lam_type 1);
 by (rtac islub_in 1);
@@ -432,8 +432,8 @@
 
 Goal  (* isub_eq *)
     "[|matrix(D,M); cpo(D)|] ==>  \
-\    isub(D,(lam n:nat. lub(D,lam m:nat. M`n`m)),y) <->  \
-\    isub(D,(lam n:nat. M`n`n),y)";
+\    isub(D,(\\<lambda>n \\<in> nat. lub(D,\\<lambda>m \\<in> nat. M`n`m)),y) <->  \
+\    isub(D,(\\<lambda>n \\<in> nat. M`n`n),y)";
 by (rtac iffI 1);
 by (rtac dominate_isub 1);
 by (assume_tac 2);
@@ -450,29 +450,29 @@
 qed "isub_eq";
 
 Goalw [lub_def]  
-    "lub(D,(lam n:nat. lub(D,lam m:nat. M`n`m))) =   \
-\    (THE x. islub(D, (lam n:nat. lub(D,lam m:nat. M`n`m)), x))";
+    "lub(D,(\\<lambda>n \\<in> nat. lub(D,\\<lambda>m \\<in> nat. M`n`m))) =   \
+\    (THE x. islub(D, (\\<lambda>n \\<in> nat. lub(D,\\<lambda>m \\<in> nat. M`n`m)), x))";
 by (Blast_tac 1);
 qed "lemma1";
 
 Goalw [lub_def]  
-    "lub(D,(lam n:nat. M`n`n)) =   \
-\    (THE x. islub(D, (lam n:nat. M`n`n), x))";
+    "lub(D,(\\<lambda>n \\<in> nat. M`n`n)) =   \
+\    (THE x. islub(D, (\\<lambda>n \\<in> nat. M`n`n), x))";
 by (Blast_tac 1);
 qed "lemma2";
 
 Goal  (* lub_matrix_diag *)
     "[|matrix(D,M); cpo(D)|] ==>  \
-\    lub(D,(lam n:nat. lub(D,lam m:nat. M`n`m))) =  \
-\    lub(D,(lam n:nat. M`n`n))";
+\    lub(D,(\\<lambda>n \\<in> nat. lub(D,\\<lambda>m \\<in> nat. M`n`m))) =  \
+\    lub(D,(\\<lambda>n \\<in> nat. M`n`n))";
 by (simp_tac (simpset() addsimps [lemma1,lemma2]) 1);
 by (asm_simp_tac (simpset() addsimps [islub_def, isub_eq]) 1);
 qed "lub_matrix_diag";
 
 Goal  (* lub_matrix_diag_sym *)
     "[|matrix(D,M); cpo(D)|] ==>  \
-\    lub(D,(lam m:nat. lub(D,lam n:nat. M`n`m))) =  \
-\    lub(D,(lam n:nat. M`n`n))";
+\    lub(D,(\\<lambda>m \\<in> nat. lub(D,\\<lambda>n \\<in> nat. M`n`m))) =  \
+\    lub(D,(\\<lambda>n \\<in> nat. M`n`n))";
 by (dtac (matrix_sym_axis RS lub_matrix_diag) 1);
 by Auto_tac;
 qed "lub_matrix_diag_sym";
@@ -482,55 +482,55 @@
 (*----------------------------------------------------------------------*)
 
 val prems = Goalw [mono_def]  (* monoI *)
-    "[|f:set(D)->set(E);   \
-\      !!x y. [|rel(D,x,y); x:set(D); y:set(D)|] ==> rel(E,f`x,f`y)|] ==>   \
-\     f:mono(D,E)";
+    "[|f \\<in> set(D)->set(E);   \
+\      !!x y. [|rel(D,x,y); x \\<in> set(D); y \\<in> set(D)|] ==> rel(E,f`x,f`y)|] ==>   \
+\     f \\<in> mono(D,E)";
 by (blast_tac(claset() addSIs prems) 1);
 qed "monoI";
 
-Goalw [mono_def] "f:mono(D,E) ==> f:set(D)->set(E)";
+Goalw [mono_def] "f \\<in> mono(D,E) ==> f \\<in> set(D)->set(E)";
 by (Fast_tac 1);
 qed "mono_fun";
 
-Goal "[|f:mono(D,E); x:set(D)|] ==> f`x:set(E)";
+Goal "[|f \\<in> mono(D,E); x \\<in> set(D)|] ==> f`x \\<in> set(E)";
 by (blast_tac(claset() addSIs [mono_fun RS apply_type]) 1);
 qed "mono_map";
 
 Goalw [mono_def]
-    "[|f:mono(D,E); rel(D,x,y); x:set(D); y:set(D)|] ==> rel(E,f`x,f`y)";
+    "[|f \\<in> mono(D,E); rel(D,x,y); x \\<in> set(D); y \\<in> set(D)|] ==> rel(E,f`x,f`y)";
 by (Blast_tac 1);
 qed "mono_mono";
 
 val prems = Goalw [cont_def,mono_def]  (* contI *)
-    "[|f:set(D)->set(E);   \
-\      !!x y. [|rel(D,x,y); x:set(D); y:set(D)|] ==> rel(E,f`x,f`y);   \
-\      !!X. chain(D,X) ==> f`lub(D,X) = lub(E,lam n:nat. f`(X`n))|] ==>   \
-\     f:cont(D,E)";
+    "[|f \\<in> set(D)->set(E);   \
+\      !!x y. [|rel(D,x,y); x \\<in> set(D); y \\<in> set(D)|] ==> rel(E,f`x,f`y);   \
+\      !!X. chain(D,X) ==> f`lub(D,X) = lub(E,\\<lambda>n \\<in> nat. f`(X`n))|] ==>   \
+\     f \\<in> cont(D,E)";
 by (fast_tac(claset() addSIs prems) 1);
 qed "contI";
 
-Goalw [cont_def] "f:cont(D,E) ==> f:mono(D,E)";
+Goalw [cont_def] "f \\<in> cont(D,E) ==> f \\<in> mono(D,E)";
 by (Blast_tac 1);
 qed "cont2mono";
 
-Goalw [cont_def] "f:cont(D,E) ==> f:set(D)->set(E)";
+Goalw [cont_def] "f \\<in> cont(D,E) ==> f \\<in> set(D)->set(E)";
 by (rtac mono_fun 1);
 by (Blast_tac 1);
 qed "cont_fun";
 
-Goal "[|f:cont(D,E); x:set(D)|] ==> f`x:set(E)";
+Goal "[|f \\<in> cont(D,E); x \\<in> set(D)|] ==> f`x \\<in> set(E)";
 by (blast_tac(claset() addSIs [cont_fun RS apply_type]) 1);
 qed "cont_map";
 
 AddTCs [comp_fun, cont_fun, cont_map];
 
 Goalw [cont_def]
-    "[|f:cont(D,E); rel(D,x,y); x:set(D); y:set(D)|] ==> rel(E,f`x,f`y)";
+    "[|f \\<in> cont(D,E); rel(D,x,y); x \\<in> set(D); y \\<in> set(D)|] ==> rel(E,f`x,f`y)";
 by (blast_tac(claset() addSIs [mono_mono]) 1);
 qed "cont_mono";
 
 Goalw [cont_def]
-    "[|f:cont(D,E); chain(D,X)|] ==> f`(lub(D,X)) = lub(E,lam n:nat. f`(X`n))";
+    "[|f \\<in> cont(D,E); chain(D,X)|] ==> f`(lub(D,X)) = lub(E,\\<lambda>n \\<in> nat. f`(X`n))";
 by (Blast_tac 1);
 qed "cont_lub";
 
@@ -538,13 +538,13 @@
 (* Continuity and chains.                                               *) 
 (*----------------------------------------------------------------------*)
 
-Goal "[|f:mono(D,E); chain(D,X)|] ==> chain(E,lam n:nat. f`(X`n))";
+Goal "[|f \\<in> mono(D,E); chain(D,X)|] ==> chain(E,\\<lambda>n \\<in> nat. f`(X`n))";
 by (simp_tac (simpset() addsimps [chain_def]) 1);
 by (blast_tac(claset() addIs [lam_type, mono_map, chain_in, 
 			      mono_mono, chain_rel]) 1);
 qed "mono_chain";
 
-Goal "[|f:cont(D,E); chain(D,X)|] ==> chain(E,lam n:nat. f`(X`n))";
+Goal "[|f \\<in> cont(D,E); chain(D,X)|] ==> chain(E,\\<lambda>n \\<in> nat. f`(X`n))";
 by (blast_tac(claset() addIs [mono_chain, cont2mono]) 1);
 qed "cont_chain";
 
@@ -554,12 +554,12 @@
 
 (* The following development more difficult with cpo-as-relation approach. *)
 
-Goalw [set_def,cf_def] "f:set(cf(D,E)) ==> f:cont(D,E)";
+Goalw [set_def,cf_def] "f \\<in> set(cf(D,E)) ==> f \\<in> cont(D,E)";
 by (Asm_full_simp_tac 1);
 qed "cf_cont";
 
 Goalw [set_def,cf_def]  (* Non-trivial with relation *)
-    "f:cont(D,E) ==> f:set(cf(D,E))";
+    "f \\<in> cont(D,E) ==> f \\<in> set(cf(D,E))";
 by (Asm_full_simp_tac 1);
 qed "cont_cf";
 
@@ -567,12 +567,12 @@
    Besides, now complicated by typing assumptions. *)
 
 val prems = Goal
-    "[|!!x. x:set(D) ==> rel(E,f`x,g`x); f:cont(D,E); g:cont(D,E)|] ==> \
+    "[|!!x. x \\<in> set(D) ==> rel(E,f`x,g`x); f \\<in> cont(D,E); g \\<in> cont(D,E)|] ==> \
 \    rel(cf(D,E),f,g)";
 by (asm_simp_tac (simpset() addsimps [rel_I, cf_def]@prems) 1);
 qed "rel_cfI";
 
-Goalw [rel_def,cf_def] "[|rel(cf(D,E),f,g); x:set(D)|] ==> rel(E,f`x,g`x)";
+Goalw [rel_def,cf_def] "[|rel(cf(D,E),f,g); x \\<in> set(D)|] ==> rel(E,f`x,g`x)";
 by (Asm_full_simp_tac 1);
 qed "rel_cf";
 
@@ -581,7 +581,7 @@
 (*----------------------------------------------------------------------*)
 
 Goal  (* chain_cf *)
-    "[| chain(cf(D,E),X); x:set(D)|] ==> chain(E,lam n:nat. X`n`x)";
+    "[| chain(cf(D,E),X); x \\<in> set(D)|] ==> chain(E,\\<lambda>n \\<in> nat. X`n`x)";
 by (rtac chainI 1);
 by (blast_tac (claset() addIs [lam_type, apply_funtype, cont_fun,
                                cf_cont,chain_in]) 1);
@@ -591,7 +591,7 @@
 
 Goal  (* matrix_lemma *)
     "[|chain(cf(D,E),X); chain(D,Xa); cpo(D); cpo(E) |] ==>   \
-\    matrix(E,lam x:nat. lam xa:nat. X`x`(Xa`xa))";
+\    matrix(E,\\<lambda>x \\<in> nat. \\<lambda>xa \\<in> nat. X`x`(Xa`xa))";
 by (rtac matrix_chainI 1);
 by Auto_tac;  
 by (rtac chainI 1);
@@ -612,7 +612,7 @@
 
 Goal  (* chain_cf_lub_cont *)
     "[|chain(cf(D,E),X); cpo(D); cpo(E) |] ==> \
-\    (lam x:set(D). lub(E, lam n:nat. X ` n ` x)) : cont(D, E)";
+\    (\\<lambda>x \\<in> set(D). lub(E, \\<lambda>n \\<in> nat. X ` n ` x)) \\<in> cont(D, E)";
 by (rtac contI 1);
 by (rtac lam_type 1);
 by (REPEAT(ares_tac[chain_cf RS cpo_lub RS islub_in] 1));
@@ -636,7 +636,7 @@
 
 Goal  (* islub_cf *)
     "[| chain(cf(D,E),X); cpo(D); cpo(E)|] ==>   \
-\     islub(cf(D,E), X, lam x:set(D). lub(E,lam n:nat. X`n`x))";
+\     islub(cf(D,E), X, \\<lambda>x \\<in> set(D). lub(E,\\<lambda>n \\<in> nat. X`n`x))";
 by (rtac islubI 1);
 by (rtac isubI 1);
 by (rtac (chain_cf_lub_cont RS cont_cf) 1);
@@ -679,11 +679,11 @@
 AddTCs [cpo_cf];
 
 Goal "[| chain(cf(D,E),X); cpo(D); cpo(E)|] ==>   \
-\     lub(cf(D,E), X) = (lam x:set(D). lub(E,lam n:nat. X`n`x))";
+\     lub(cf(D,E), X) = (\\<lambda>x \\<in> set(D). lub(E,\\<lambda>n \\<in> nat. X`n`x))";
 by (blast_tac (claset() addIs [islub_unique,cpo_lub,islub_cf,cpo_cf]) 1);
 qed "lub_cf";
 
-Goal "[|y:set(E); cpo(D); cpo(E)|] ==> (lam x:set(D).y) : cont(D,E)";
+Goal "[|y \\<in> set(E); cpo(D); cpo(E)|] ==> (\\<lambda>x \\<in> set(D).y) \\<in> cont(D,E)";
 by (rtac contI 1);
 by (Asm_simp_tac 2);
 by (blast_tac (claset() addIs [lam_type]) 1);
@@ -691,7 +691,7 @@
 				     lub_const]) 1);
 qed "const_cont";
 
-Goal "[|cpo(D); pcpo(E); y:cont(D,E)|]==>rel(cf(D,E),(lam x:set(D).bot(E)),y)";
+Goal "[|cpo(D); pcpo(E); y \\<in> cont(D,E)|]==>rel(cf(D,E),(\\<lambda>x \\<in> set(D).bot(E)),y)";
 by (rtac rel_cfI 1);
 by (Asm_simp_tac 1);
 by (ALLGOALS (type_solver_tac (tcset() addTCs [cont_fun, const_cont]) []));
@@ -704,7 +704,7 @@
 qed "pcpo_cf";
 
 Goal  (* bot_cf *)
-    "[|cpo(D); pcpo(E)|] ==> bot(cf(D,E)) = (lam x:set(D).bot(E))";
+    "[|cpo(D); pcpo(E)|] ==> bot(cf(D,E)) = (\\<lambda>x \\<in> set(D).bot(E))";
 by (blast_tac (claset() addIs [bot_unique RS sym, pcpo_cf, cf_least, 
                    bot_in RS const_cont RS cont_cf, cf_cont, pcpo_cpo])1);
 qed "bot_cf";
@@ -724,7 +724,7 @@
 val comp_cont_apply = cont_fun RSN(2,cont_fun RS comp_fun_apply);
 
 Goal  (* comp_pres_cont *)
-    "[| f:cont(D',E); g:cont(D,D'); cpo(D)|] ==> f O g : cont(D,E)";
+    "[| f \\<in> cont(D',E); g \\<in> cont(D,D'); cpo(D)|] ==> f O g \\<in> cont(D,E)";
 by (rtac contI 1);
 by (stac comp_cont_apply 2);
 by (stac comp_cont_apply 5);
@@ -741,7 +741,7 @@
 AddTCs [comp_pres_cont];
 
 Goal  (* comp_mono *)
-    "[| f:cont(D',E); g:cont(D,D'); f':cont(D',E); g':cont(D,D');   \
+    "[| f \\<in> cont(D',E); g \\<in> cont(D,D'); f':cont(D',E); g':cont(D,D');   \
 \       rel(cf(D',E),f,f'); rel(cf(D,D'),g,g'); cpo(D); cpo(E) |] ==>   \
 \    rel(cf(D,E),f O g,f' O g')";
 by (rtac rel_cfI 1); (* extra proof obl: f O g and f' O g' cont. Extra asm cpo(D). *)
@@ -753,7 +753,7 @@
 
 Goal  (* chain_cf_comp *)
     "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(E)|] ==>  \
-\    chain(cf(D,E),lam n:nat. X`n O Y`n)";
+\    chain(cf(D,E),\\<lambda>n \\<in> nat. X`n O Y`n)";
 by (rtac chainI 1);
 by (Asm_simp_tac 2);
 by (rtac rel_cfI 2);
@@ -767,7 +767,7 @@
 
 Goal  (* comp_lubs *)
     "[| chain(cf(D',E),X); chain(cf(D,D'),Y); cpo(D); cpo(D'); cpo(E)|] ==>  \
-\    lub(cf(D',E),X) O lub(cf(D,D'),Y) = lub(cf(D,E),lam n:nat. X`n O Y`n)";
+\    lub(cf(D',E),X) O lub(cf(D,D'),Y) = lub(cf(D,E),\\<lambda>n \\<in> nat. X`n O Y`n)";
 by (rtac fun_extension 1);
 by (stac lub_cf 3);
 brr[comp_fun, cf_cont RS cont_fun, cpo_lub RS islub_in, cpo_cf, chain_cf_comp] 1;
@@ -780,7 +780,7 @@
 by (asm_simp_tac(simpset() addsimps
 		 [lub_cf,chain_cf, chain_in RS cf_cont RS cont_lub,
 		  chain_cf RS cpo_lub RS islub_in]) 1);
-by (cut_inst_tac[("M","lam xa:nat. lam xb:nat. X`xa`(Y`xb`x)")]
+by (cut_inst_tac[("M","\\<lambda>xa \\<in> nat. \\<lambda>xb \\<in> nat. X`xa`(Y`xb`x)")]
    lub_matrix_diag 1);
 by (Asm_full_simp_tac 3);
 by (rtac matrix_chainI 1);
@@ -799,16 +799,16 @@
 (*----------------------------------------------------------------------*)
 
 Goalw [projpair_def]  (* projpairI *)
-    "[| e:cont(D,E); p:cont(E,D); p O e = id(set(D));   \
+    "[| e \\<in> cont(D,E); p \\<in> cont(E,D); p O e = id(set(D));   \
 \       rel(cf(E,E))(e O p)(id(set(E)))|] ==> projpair(D,E,e,p)";
 by (Fast_tac 1);
 qed "projpairI";
 
-Goalw [projpair_def] "projpair(D,E,e,p) ==> e:cont(D,E)";
+Goalw [projpair_def] "projpair(D,E,e,p) ==> e \\<in> cont(D,E)";
 by Auto_tac;  
 qed "projpair_e_cont";
 
-Goalw [projpair_def] "projpair(D,E,e,p) ==> p:cont(E,D)";
+Goalw [projpair_def] "projpair(D,E,e,p) ==> p \\<in> cont(E,D)";
 by Auto_tac;  
 qed "projpair_p_cont";
 
@@ -824,7 +824,7 @@
 
 (*----------------------------------------------------------------------*)
 (* NB! projpair_e_cont and projpair_p_cont cannot be used repeatedly    *)
-(*     at the same time since both match a goal of the form f:cont(X,Y).*)
+(*     at the same time since both match a goal of the form f \\<in> cont(X,Y).*)
 (*----------------------------------------------------------------------*)
 
 (*----------------------------------------------------------------------*)
@@ -923,7 +923,7 @@
 by (blast_tac (claset() addIs [embRp, embI, projpair_unique RS iffD1]) 1);
 qed "Rp_unique";
 
-Goalw [emb_def] "emb(D,E,e) ==> e:cont(D,E)";
+Goalw [emb_def] "emb(D,E,e) ==> e \\<in> cont(D,E)";
 by (blast_tac (claset() addIs [projpair_e_cont]) 1);
 qed "emb_cont";
 
@@ -936,7 +936,7 @@
 AddTCs [emb_cont, Rp_cont];
 
 Goal  (* embRp_eq_thm *)
-    "[|emb(D,E,e); x:set(D); cpo(D); cpo(E)|] ==> Rp(D,E,e)`(e`x) = x";
+    "[|emb(D,E,e); x \\<in> set(D); cpo(D); cpo(E)|] ==> Rp(D,E,e)`(e`x) = x";
 by (rtac (comp_fun_apply RS subst) 1);
 brr[Rp_cont,emb_cont,cont_fun] 1;
 by (stac embRp_eq 1);
@@ -1013,20 +1013,20 @@
 (*----------------------------------------------------------------------*)
 
 Goalw [set_def,iprod_def]  (* iprodI *)
-    "x:(PROD n:nat. set(DD`n)) ==> x:set(iprod(DD))";
+    "x:(\\<Pi>n \\<in> nat. set(DD`n)) ==> x \\<in> set(iprod(DD))";
 by (Asm_full_simp_tac 1);
 qed "iprodI";
 
 Goalw [set_def,iprod_def]  (* iprodE *)
-    "x:set(iprod(DD)) ==> x:(PROD n:nat. set(DD`n))";
+    "x \\<in> set(iprod(DD)) ==> x:(\\<Pi>n \\<in> nat. set(DD`n))";
 by (Asm_full_simp_tac 1);
 qed "iprodE";
 
 (* Contains typing conditions in contrast to HOL-ST *)
 
 val prems = Goalw [iprod_def] (* rel_iprodI *)
-    "[|!!n. n:nat ==> rel(DD`n,f`n,g`n); f:(PROD n:nat. set(DD`n));  \
-\      g:(PROD n:nat. set(DD`n))|] ==> rel(iprod(DD),f,g)";
+    "[|!!n. n \\<in> nat ==> rel(DD`n,f`n,g`n); f:(\\<Pi>n \\<in> nat. set(DD`n));  \
+\      g:(\\<Pi>n \\<in> nat. set(DD`n))|] ==> rel(iprod(DD),f,g)";
 by (rtac rel_I 1);
 by (Simp_tac 1);
 by Safe_tac;
@@ -1034,7 +1034,7 @@
 qed "rel_iprodI";
 
 Goalw [iprod_def]
-    "[|rel(iprod(DD),f,g); n:nat|] ==> rel(DD`n,f`n,g`n)";
+    "[|rel(iprod(DD),f,g); n \\<in> nat|] ==> rel(DD`n,f`n,g`n)";
 by (fast_tac (claset() addDs [rel_E] addss simpset()) 1);
 qed "rel_iprodE";
 
@@ -1042,8 +1042,8 @@
    probably not needed in Isabelle, wait and see. *)
 
 val prems = Goalw [chain_def]  (* chain_iprod *)
-    "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n); n:nat|] ==>  \
-\    chain(DD`n,lam m:nat. X`m`n)";
+    "[|chain(iprod(DD),X);  !!n. n \\<in> nat ==> cpo(DD`n); n \\<in> nat|] ==>  \
+\    chain(DD`n,\\<lambda>m \\<in> nat. X`m`n)";
 by Safe_tac;
 by (rtac lam_type 1);
 by (rtac apply_type 1);
@@ -1057,8 +1057,8 @@
 qed "chain_iprod";
 
 val prems = Goalw [islub_def,isub_def]  (* islub_iprod *)
-    "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n)|] ==>   \
-\    islub(iprod(DD),X,lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
+    "[|chain(iprod(DD),X);  !!n. n \\<in> nat ==> cpo(DD`n)|] ==>   \
+\    islub(iprod(DD),X,\\<lambda>n \\<in> nat. lub(DD`n,\\<lambda>m \\<in> nat. X`m`n))";
 by Safe_tac;
 by (rtac iprodI 1);
 by (rtac lam_type 1); 
@@ -1066,7 +1066,7 @@
 by (rtac rel_iprodI 1);
 by (Asm_simp_tac 1);
 (* Here, HOL resolution is handy, Isabelle resolution bad. *)
-by (res_inst_tac[("P","%t. rel(DD`na,t,lub(DD`na,lam x:nat. X`x`na))"),
+by (res_inst_tac[("P","%t. rel(DD`na,t,lub(DD`na,\\<lambda>x \\<in> nat. X`x`na))"),
     ("b1","%n. X`n`na")](beta RS subst) 1);
 brr((chain_iprod RS cpo_lub RS islub_ub)::iprodE::chain_in::prems) 1;
 brr(iprodI::lam_type::(chain_iprod RS cpo_lub RS islub_in)::prems) 1;
@@ -1084,7 +1084,7 @@
 qed "islub_iprod";
 
 val prems = Goal (* cpo_iprod *)
-    "(!!n. n:nat ==> cpo(DD`n)) ==> cpo(iprod(DD))";
+    "(!!n. n \\<in> nat ==> cpo(DD`n)) ==> cpo(iprod(DD))";
 brr[cpoI,poI] 1;
 by (rtac rel_iprodI 1); (* not repeated: want to solve 1 and leave 2 unchanged *)
 brr(cpo_refl::(iprodE RS apply_type)::iprodE::prems) 1;
@@ -1100,8 +1100,8 @@
 AddTCs [cpo_iprod];
 
 val prems = Goalw [islub_def,isub_def]  (* lub_iprod *)
-    "[|chain(iprod(DD),X);  !!n. n:nat ==> cpo(DD`n)|] ==>   \
-\    lub(iprod(DD),X) = (lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
+    "[|chain(iprod(DD),X);  !!n. n \\<in> nat ==> cpo(DD`n)|] ==>   \
+\    lub(iprod(DD),X) = (\\<lambda>n \\<in> nat. lub(DD`n,\\<lambda>m \\<in> nat. X`m`n))";
 brr((cpo_lub RS islub_unique)::islub_iprod::cpo_iprod::prems) 1;
 qed "lub_iprod";
 
@@ -1111,8 +1111,8 @@
 
 val prems = Goalw [subcpo_def]  (* subcpoI *)
     "[|set(D)<=set(E);  \
-\      !!x y. [|x:set(D); y:set(D)|] ==> rel(D,x,y)<->rel(E,x,y);  \
-\      !!X. chain(D,X) ==> lub(E,X) : set(D)|] ==> subcpo(D,E)";
+\      !!x y. [|x \\<in> set(D); y \\<in> set(D)|] ==> rel(D,x,y)<->rel(E,x,y);  \
+\      !!X. chain(D,X) ==> lub(E,X) \\<in> set(D)|] ==> subcpo(D,E)";
 by Safe_tac;
 by (asm_full_simp_tac(simpset() addsimps prems) 2);
 by (asm_simp_tac(simpset() addsimps prems) 2);
@@ -1124,14 +1124,14 @@
 qed "subcpo_subset";
 
 Goalw [subcpo_def]  
-    "[|subcpo(D,E); x:set(D); y:set(D)|] ==> rel(D,x,y)<->rel(E,x,y)";
+    "[|subcpo(D,E); x \\<in> set(D); y \\<in> set(D)|] ==> rel(D,x,y)<->rel(E,x,y)";
 by (Blast_tac 1);
 qed "subcpo_rel_eq";
 
 val subcpo_relD1 = subcpo_rel_eq RS iffD1;
 val subcpo_relD2 = subcpo_rel_eq RS iffD2;
 
-Goalw [subcpo_def] "[|subcpo(D,E); chain(D,X)|] ==> lub(E,X) : set(D)";
+Goalw [subcpo_def] "[|subcpo(D,E); chain(D,X)|] ==> lub(E,X) \\<in> set(D)";
 by (Blast_tac 1);
 qed "subcpo_lub";
 
@@ -1180,7 +1180,7 @@
 (* Making subcpos using mkcpo.                                          *)
 (*----------------------------------------------------------------------*)
 
-Goalw [set_def,mkcpo_def] "[|x:set(D); P(x)|] ==> x:set(mkcpo(D,P))";
+Goalw [set_def,mkcpo_def] "[|x \\<in> set(D); P(x)|] ==> x \\<in> set(mkcpo(D,P))";
 by Auto_tac;
 qed "mkcpoI";
 
@@ -1206,12 +1206,12 @@
 *)
 
 Goalw [set_def,mkcpo_def]  (* mkcpoD1 *)
-    "x:set(mkcpo(D,P))==> x:set(D)";
+    "x \\<in> set(mkcpo(D,P))==> x \\<in> set(D)";
 by (Asm_full_simp_tac 1);
 qed "mkcpoD1";
 
 Goalw [set_def,mkcpo_def]  (* mkcpoD2 *)
-    "x:set(mkcpo(D,P))==> P(x)";
+    "x \\<in> set(mkcpo(D,P))==> P(x)";
 by (Asm_full_simp_tac 1);
 qed "mkcpoD2";
 
@@ -1221,7 +1221,7 @@
 qed "rel_mkcpoE";
 
 Goalw [mkcpo_def,rel_def,set_def]
-    "[|x:set(D); y:set(D)|] ==> rel(mkcpo(D,P),x,y) <-> rel(D,x,y)";
+    "[|x \\<in> set(D); y \\<in> set(D)|] ==> rel(mkcpo(D,P),x,y) <-> rel(D,x,y)";
 by Auto_tac;  
 qed "rel_mkcpo";
 
@@ -1247,20 +1247,20 @@
 (*----------------------------------------------------------------------*)
 
 val prems = Goalw [emb_chain_def]  (* emb_chainI *)
-    "[|!!n. n:nat ==> cpo(DD`n);   \
-\      !!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n)|] ==> emb_chain(DD,ee)";
+    "[|!!n. n \\<in> nat ==> cpo(DD`n);   \
+\      !!n. n \\<in> nat ==> emb(DD`n,DD`succ(n),ee`n)|] ==> emb_chain(DD,ee)";
 by Safe_tac;
 by (REPEAT (ares_tac prems 1));
 qed "emb_chainI";
 
-Goalw [emb_chain_def] "[|emb_chain(DD,ee); n:nat|] ==> cpo(DD`n)";
+Goalw [emb_chain_def] "[|emb_chain(DD,ee); n \\<in> nat|] ==> cpo(DD`n)";
 by (Fast_tac 1);
 qed "emb_chain_cpo";
 
 AddTCs [emb_chain_cpo];
 
 Goalw [emb_chain_def] 
-    "[|emb_chain(DD,ee); n:nat|] ==> emb(DD`n,DD`succ(n),ee`n)";
+    "[|emb_chain(DD,ee); n \\<in> nat|] ==> emb(DD`n,DD`succ(n),ee`n)";
 by (Fast_tac 1);
 qed "emb_chain_emb";
 
@@ -1269,31 +1269,31 @@
 (*----------------------------------------------------------------------*)
 
 val prems = Goalw [Dinf_def]  (* DinfI *)
-    "[|x:(PROD n:nat. set(DD`n));  \
-\      !!n. n:nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|] ==>   \
-\    x:set(Dinf(DD,ee))";
+    "[|x:(\\<Pi>n \\<in> nat. set(DD`n));  \
+\      !!n. n \\<in> nat ==> Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n|] ==>   \
+\    x \\<in> set(Dinf(DD,ee))";
 brr(mkcpoI::iprodI::ballI::prems) 1;
 qed "DinfI";
 
-Goalw [Dinf_def] "x:set(Dinf(DD,ee)) ==> x:(PROD n:nat. set(DD`n))";
+Goalw [Dinf_def] "x \\<in> set(Dinf(DD,ee)) ==> x:(\\<Pi>n \\<in> nat. set(DD`n))";
 by (etac (mkcpoD1 RS iprodE) 1);
 qed "Dinf_prod";
 
 Goalw [Dinf_def]
-    "[|x:set(Dinf(DD,ee)); n:nat|] ==>   \
+    "[|x \\<in> set(Dinf(DD,ee)); n \\<in> nat|] ==>   \
 \    Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n";
 by (blast_tac (claset() addDs [mkcpoD2])  1);
 qed "Dinf_eq";
 
 val prems = Goalw [Dinf_def] 
-    "[|!!n. n:nat ==> rel(DD`n,x`n,y`n);  \
-\      x:(PROD n:nat. set(DD`n)); y:(PROD n:nat. set(DD`n))|] ==>   \
+    "[|!!n. n \\<in> nat ==> rel(DD`n,x`n,y`n);  \
+\      x:(\\<Pi>n \\<in> nat. set(DD`n)); y:(\\<Pi>n \\<in> nat. set(DD`n))|] ==>   \
 \    rel(Dinf(DD,ee),x,y)";
 by (rtac (rel_mkcpo RS iffD2) 1);
 brr(rel_iprodI::iprodI::prems) 1;
 qed "rel_DinfI";
 
-Goalw [Dinf_def] "[|rel(Dinf(DD,ee),x,y); n:nat|] ==> rel(DD`n,x`n,y`n)";
+Goalw [Dinf_def] "[|rel(Dinf(DD,ee),x,y); n \\<in> nat|] ==> rel(DD`n,x`n,y`n)";
 by (etac (rel_mkcpoE RS rel_iprodE) 1);
 by (assume_tac 1);
 qed "rel_Dinf";
@@ -1330,7 +1330,7 @@
 
 Goal  (* lub_Dinf *)
     "[|chain(Dinf(DD,ee),X); emb_chain(DD,ee)|] ==>  \
-\    lub(Dinf(DD,ee),X) = (lam n:nat. lub(DD`n,lam m:nat. X`m`n))";
+\    lub(Dinf(DD,ee),X) = (\\<lambda>n \\<in> nat. lub(DD`n,\\<lambda>m \\<in> nat. X`m`n))";
 by (stac (subcpo_Dinf RS lub_subcpo) 1);
 by (auto_tac (claset() addIs [cpo_iprod,emb_chain_cpo,lub_iprod,chain_Dinf], simpset()));
 qed "lub_Dinf";
@@ -1341,7 +1341,7 @@
 (*----------------------------------------------------------------------*)
 
 Goalw [e_less_def]  (* e_less_eq *)
-    "m:nat ==> e_less(DD,ee,m,m) = id(set(DD`m))";
+    "m \\<in> nat ==> e_less(DD,ee,m,m) = id(set(DD`m))";
 by (asm_simp_tac (simpset() addsimps[diff_self_eq_0]) 1);
 qed "e_less_eq";
  
@@ -1354,22 +1354,22 @@
 by (asm_simp_tac (simpset() addsimps [lemma_succ_sub,diff_add_inverse]) 1);
 qed "e_less_add";
 
-Goal "n:nat ==> succ(n) = n #+ 1";
+Goal "n \\<in> nat ==> succ(n) = n #+ 1";
 by (Asm_simp_tac 1);
 qed "add1";
 
-Goal "[| m le n; n: nat |] ==> EX k: nat. n = m #+ k";
+Goal "[| m le n; n \\<in> nat |] ==> \\<exists>k \\<in> nat. n = m #+ k";
 by (dtac less_imp_succ_add 1);
 by Auto_tac;  
 val lemma_le_exists = result();
 
 val prems = Goal
-    "[| m le n;  !!x. [|n=m#+x; x:nat|] ==> Q;  n:nat |] ==> Q";
+    "[| m le n;  !!x. [|n=m#+x; x \\<in> nat|] ==> Q;  n \\<in> nat |] ==> Q";
 by (rtac (lemma_le_exists RS bexE) 1);
 by (DEPTH_SOLVE (ares_tac prems 1));
 qed "le_exists";
 
-Goal "[| m le n;  n:nat |] ==>   \
+Goal "[| m le n;  n \\<in> nat |] ==>   \
 \     e_less(DD,ee,m,succ(n)) = ee`n O e_less(DD,ee,m,n)";
 by (rtac le_exists 1);
 by (assume_tac 1);
@@ -1379,12 +1379,12 @@
 
 (* All theorems assume variables m and n are natural numbers. *)
 
-Goal "m:nat ==> e_less(DD,ee,m,succ(m)) = ee`m O id(set(DD`m))";
+Goal "m \\<in> nat ==> e_less(DD,ee,m,succ(m)) = ee`m O id(set(DD`m))";
 by (asm_simp_tac(simpset() addsimps[e_less_le, e_less_eq]) 1);
 qed "e_less_succ";
 
 val prems = Goal
-    "[|!!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n); m:nat|] ==>   \
+    "[|!!n. n \\<in> nat ==> emb(DD`n,DD`succ(n),ee`n); m \\<in> nat|] ==>   \
 \    e_less(DD,ee,m,succ(m)) = ee`m";
 by (asm_simp_tac(simpset() addsimps e_less_succ::prems) 1);
 by (stac comp_id 1);
@@ -1394,7 +1394,7 @@
 (* Compare this proof with the HOL one, here we do type checking. *)
 (* In any case the one below was very easy to write. *)
 
-Goal "[| emb_chain(DD,ee); m:nat |] ==>   \
+Goal "[| emb_chain(DD,ee); m \\<in> nat |] ==>   \
 \     emb(DD`m, DD`(m#+k), e_less(DD,ee,m,m#+k))";
 by (subgoal_tac "emb(DD`m, DD`(m#+natify(k)), e_less(DD,ee,m,m#+natify(k)))" 1);
 by (res_inst_tac [("n","natify(k)")] nat_induct 2);
@@ -1405,7 +1405,7 @@
 	      simpset()));
 qed "emb_e_less_add";
 
-Goal "[| m le n;  emb_chain(DD,ee);  n:nat |] ==>   \
+Goal "[| m le n;  emb_chain(DD,ee);  n \\<in> nat |] ==>   \
 \    emb(DD`m, DD`n, e_less(DD,ee,m,n))";
 by (ftac lt_nat_in_nat 1);
 by (etac nat_succI 1);
@@ -1427,7 +1427,7 @@
    Therefore this theorem is only a lemma. *)
 
 Goal  (* e_less_split_add_lemma *)
-    "[| emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[| emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    n le k --> \
 \    e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)";
 by (induct_tac "k" 1);
@@ -1449,38 +1449,38 @@
 		      nat_succI] 1));
 qed "e_less_split_add_lemma";
 
-Goal "[| n le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+Goal "[| n le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \     e_less(DD,ee,m,m#+k) = e_less(DD,ee,m#+n,m#+k) O e_less(DD,ee,m,m#+n)";
 by (blast_tac (claset() addIs [e_less_split_add_lemma RS mp]) 1);
 qed "e_less_split_add";
 
 Goalw [e_gr_def]  (* e_gr_eq *)
-    "m:nat ==> e_gr(DD,ee,m,m) = id(set(DD`m))";
+    "m \\<in> nat ==> e_gr(DD,ee,m,m) = id(set(DD`m))";
 by (asm_simp_tac (simpset() addsimps[diff_self_eq_0]) 1);
 qed "e_gr_eq";
 
 Goalw [e_gr_def] (* e_gr_add *)
-    "[|n:nat; k:nat|] ==>    \
+    "[|n \\<in> nat; k \\<in> nat|] ==>    \
 \         e_gr(DD,ee,succ(n#+k),n) =   \
 \         e_gr(DD,ee,n#+k,n) O Rp(DD`(n#+k),DD`succ(n#+k),ee`(n#+k))";
 by (asm_simp_tac (simpset() addsimps [lemma_succ_sub,diff_add_inverse]) 1);
 qed "e_gr_add";
 
-Goal "[|n le m; m:nat; n:nat|] ==>   \
+Goal "[|n le m; m \\<in> nat; n \\<in> nat|] ==>   \
 \    e_gr(DD,ee,succ(m),n) = e_gr(DD,ee,m,n) O Rp(DD`m,DD`succ(m),ee`m)";
 by (etac le_exists 1);
 by (asm_simp_tac(simpset() addsimps[e_gr_add]) 1);
 by (REPEAT (assume_tac 1));
 qed "e_gr_le";
 
-Goal "m:nat ==>   \
+Goal "m \\<in> nat ==>   \
 \    e_gr(DD,ee,succ(m),m) = id(set(DD`m)) O Rp(DD`m,DD`succ(m),ee`m)";
 by (asm_simp_tac(simpset() addsimps[e_gr_le,e_gr_eq]) 1);
 qed "e_gr_succ";
 
 (* Cpo asm's due to THE uniqueness. *)
 
-Goal "[|emb_chain(DD,ee); m:nat|] ==>   \
+Goal "[|emb_chain(DD,ee); m \\<in> nat|] ==>   \
 \    e_gr(DD,ee,succ(m),m) = Rp(DD`m,DD`succ(m),ee`m)";
 by (asm_simp_tac(simpset() addsimps[e_gr_succ]) 1);
 by (blast_tac (claset() addIs [id_comp, Rp_cont,cont_fun,
@@ -1488,7 +1488,7 @@
 qed "e_gr_succ_emb";
 
 Goal  (* e_gr_fun_add *)
-    "[|emb_chain(DD,ee); n:nat; k:nat|] ==>   \
+    "[|emb_chain(DD,ee); n \\<in> nat; k \\<in> nat|] ==>   \
 \    e_gr(DD,ee,n#+k,n): set(DD`(n#+k))->set(DD`n)";
 by (induct_tac "k" 1);
 by (asm_simp_tac(simpset() addsimps[e_gr_eq,id_type]) 1);
@@ -1497,7 +1497,7 @@
 qed "e_gr_fun_add";
 
 Goal  (* e_gr_fun *)
-    "[|n le m; emb_chain(DD,ee); m:nat; n:nat|] ==>   \
+    "[|n le m; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat|] ==>   \
 \    e_gr(DD,ee,m,n): set(DD`m)->set(DD`n)";
 by (rtac le_exists 1);
 by (assume_tac 1);
@@ -1506,7 +1506,7 @@
 qed "e_gr_fun";
 
 Goal  (* e_gr_split_add_lemma *)
-    "[| emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[| emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    m le k --> \
 \    e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)";
 by (induct_tac "k" 1);
@@ -1530,18 +1530,18 @@
 by (REPEAT (ares_tac [e_gr_fun,add_type,refl,add_le_self,nat_succI] 1));
 qed "e_gr_split_add_lemma";
 
-Goal "[| m le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+Goal "[| m le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \     e_gr(DD,ee,n#+k,n) = e_gr(DD,ee,n#+m,n) O e_gr(DD,ee,n#+k,n#+m)";
 by (blast_tac (claset() addIs [e_gr_split_add_lemma RS mp]) 1);
 qed "e_gr_split_add";
 
-Goal "[|m le n; emb_chain(DD,ee); m:nat; n:nat|] ==>   \
+Goal "[|m le n; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat|] ==>   \
 \     e_less(DD,ee,m,n):cont(DD`m,DD`n)";
 by (blast_tac (claset() addIs [emb_cont, emb_e_less]) 1);
 qed "e_less_cont";
 
 Goal  (* e_gr_cont *)
-    "[|n le m; emb_chain(DD,ee); m:nat; n:nat|] ==>   \
+    "[|n le m; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat|] ==>   \
 \    e_gr(DD,ee,m,n):cont(DD`m,DD`n)";
 by (etac rev_mp 1);
 by (induct_tac "m" 1);
@@ -1560,7 +1560,7 @@
 (* Considerably shorter.... 57 against 26 *)
 
 Goal  (* e_less_e_gr_split_add *)
-    "[|n le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>   \
+    "[|n le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>   \
 \    e_less(DD,ee,m,m#+n) = e_gr(DD,ee,m#+k,m#+n) O e_less(DD,ee,m,m#+k)";
 (* Use mp to prepare for induction. *)
 by (etac rev_mp 1);
@@ -1588,7 +1588,7 @@
 (* Again considerably shorter, and easy to obtain from the previous thm. *)
 
 Goal  (* e_gr_e_less_split_add *)
-    "[|m le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>   \
+    "[|m le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>   \
 \    e_gr(DD,ee,n#+m,n) = e_gr(DD,ee,n#+k,n) O e_less(DD,ee,n#+m,n#+k)";
 (* Use mp to prepare for induction. *)
 by (etac rev_mp 1);
@@ -1615,14 +1615,14 @@
 
 
 Goalw [eps_def]  (* emb_eps *)
-    "[|m le n; emb_chain(DD,ee); m:nat; n:nat|] ==>   \
+    "[|m le n; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat|] ==>   \
 \    emb(DD`m,DD`n,eps(DD,ee,m,n))";
 by (asm_simp_tac(simpset()) 1);
 brr[emb_e_less] 1;
 qed "emb_eps";
 
 Goalw [eps_def]  (* eps_fun *)
-    "[|emb_chain(DD,ee); m:nat; n:nat|] ==>   \
+    "[|emb_chain(DD,ee); m \\<in> nat; n \\<in> nat|] ==>   \
 \    eps(DD,ee,m,n): set(DD`m)->set(DD`n)";
 by (rtac (split_if RS iffD2) 1);
 by Safe_tac;
@@ -1630,22 +1630,22 @@
 by (auto_tac (claset() addIs [not_le_iff_lt RS iffD1 RS leI, e_gr_fun,nat_into_Ord], simpset()));
 qed "eps_fun";
 
-Goalw [eps_def] "n:nat ==> eps(DD,ee,n,n) = id(set(DD`n))";
+Goalw [eps_def] "n \\<in> nat ==> eps(DD,ee,n,n) = id(set(DD`n))";
 by (asm_simp_tac(simpset() addsimps [e_less_eq]) 1);
 qed "eps_id";
 
 Goalw [eps_def]
-    "[|m:nat; n:nat|] ==> eps(DD,ee,m,m#+n) = e_less(DD,ee,m,m#+n)";
+    "[|m \\<in> nat; n \\<in> nat|] ==> eps(DD,ee,m,m#+n) = e_less(DD,ee,m,m#+n)";
 by (asm_simp_tac(simpset() addsimps [add_le_self]) 1);
 qed "eps_e_less_add";
 
 Goalw [eps_def]
-    "[|m le n; m:nat; n:nat|] ==> eps(DD,ee,m,n) = e_less(DD,ee,m,n)";
+    "[|m le n; m \\<in> nat; n \\<in> nat|] ==> eps(DD,ee,m,n) = e_less(DD,ee,m,n)";
 by (Asm_simp_tac 1);
 qed "eps_e_less";
 
 Goalw [eps_def]  (* eps_e_gr_add *)
-    "[|n:nat; k:nat|] ==> eps(DD,ee,n#+k,n) = e_gr(DD,ee,n#+k,n)";
+    "[|n \\<in> nat; k \\<in> nat|] ==> eps(DD,ee,n#+k,n) = e_gr(DD,ee,n#+k,n)";
 by (rtac (split_if RS iffD2) 1);
 by Safe_tac;
 by (etac leE 1);
@@ -1658,7 +1658,7 @@
 qed "eps_e_gr_add";
 
 Goal  (* eps_e_gr *)
-    "[|n le m; m:nat; n:nat|] ==> eps(DD,ee,m,n) = e_gr(DD,ee,m,n)";
+    "[|n le m; m \\<in> nat; n \\<in> nat|] ==> eps(DD,ee,m,n) = e_gr(DD,ee,m,n)";
 by (rtac le_exists 1);
 by (assume_tac 1);
 by (asm_simp_tac(simpset() addsimps[eps_e_gr_add]) 1);
@@ -1666,21 +1666,21 @@
 qed "eps_e_gr";
 
 val prems = Goal  (* eps_succ_ee *)
-    "[|!!n. n:nat ==> emb(DD`n,DD`succ(n),ee`n); m:nat|] ==>  \
+    "[|!!n. n \\<in> nat ==> emb(DD`n,DD`succ(n),ee`n); m \\<in> nat|] ==>  \
 \    eps(DD,ee,m,succ(m)) = ee`m";
 by (asm_simp_tac(simpset() addsimps eps_e_less::le_succ_iff::e_less_succ_emb::
    prems) 1);
 qed "eps_succ_ee";
 
 Goal  (* eps_succ_Rp *)
-    "[|emb_chain(DD,ee); m:nat|] ==>  \
+    "[|emb_chain(DD,ee); m \\<in> nat|] ==>  \
 \    eps(DD,ee,succ(m),m) = Rp(DD`m,DD`succ(m),ee`m)";
 by (asm_simp_tac(simpset() addsimps eps_e_gr::le_succ_iff::e_gr_succ_emb::
    prems) 1);
 qed "eps_succ_Rp";
 
 Goal  (* eps_cont *)
-    "[|emb_chain(DD,ee); m:nat; n:nat|] ==> eps(DD,ee,m,n): cont(DD`m,DD`n)";
+    "[|emb_chain(DD,ee); m \\<in> nat; n \\<in> nat|] ==> eps(DD,ee,m,n): cont(DD`m,DD`n)";
 by (res_inst_tac [("i","m"),("j","n")] nat_linear_le 1);
 by (ALLGOALS (asm_simp_tac(simpset() addsimps [eps_e_less,e_less_cont,
 					       eps_e_gr,e_gr_cont])));     
@@ -1689,7 +1689,7 @@
 (* Theorems about splitting. *)
 
 Goal  (* eps_split_add_left *)
-    "[|n le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|n le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,m,m#+k) = eps(DD,ee,m#+n,m#+k) O eps(DD,ee,m,m#+n)";
 by (asm_simp_tac(simpset() addsimps 
     [eps_e_less,add_le_self,add_le_mono]) 1);
@@ -1697,7 +1697,7 @@
 qed "eps_split_add_left";
 
 Goal  (* eps_split_add_left_rev *)
-    "[|n le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|n le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,m,m#+n) = eps(DD,ee,m#+k,m#+n) O eps(DD,ee,m,m#+k)";
 by (asm_simp_tac(simpset() addsimps 
     [eps_e_less_add,eps_e_gr,add_le_self,add_le_mono]) 1);
@@ -1705,7 +1705,7 @@
 qed "eps_split_add_left_rev";
 
 Goal  (* eps_split_add_right *)
-    "[|m le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|m le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,n#+k,n) = eps(DD,ee,n#+m,n) O eps(DD,ee,n#+k,n#+m)";
 by (asm_simp_tac(simpset() addsimps 
     [eps_e_gr,add_le_self,add_le_mono]) 1);
@@ -1713,7 +1713,7 @@
 qed "eps_split_add_right";
 
 Goal  (* eps_split_add_right_rev *)
-    "[|m le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|m le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,n#+m,n) = eps(DD,ee,n#+k,n) O eps(DD,ee,n#+m,n#+k)";
 by (asm_simp_tac(simpset() addsimps 
     [eps_e_gr_add,eps_e_less,add_le_self,add_le_mono]) 1);
@@ -1724,8 +1724,8 @@
 
 val [prem1,prem2,prem3,prem4] = Goal
     "[| n le k; k le m;  \
-\       !!p q. [|p le q; k=n#+p; m=n#+q; p:nat; q:nat|] ==> R; \
-\       m:nat |]==>R";
+\       !!p q. [|p le q; k=n#+p; m=n#+q; p \\<in> nat; q \\<in> nat|] ==> R; \
+\       m \\<in> nat |]==>R";
 by (rtac (prem1 RS le_exists) 1);
 by (simp_tac (simpset() addsimps [prem2 RS lt_nat_in_nat, prem4]) 2);
 by (rtac ([prem1,prem2] MRS le_trans RS le_exists) 1);
@@ -1738,7 +1738,7 @@
 qed "le_exists_lemma";
 
 Goal  (* eps_split_left_le *)
-    "[|m le k; k le n; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|m le k; k le n; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)";
 by (rtac le_exists_lemma 1);
 by (REPEAT (assume_tac 1));
@@ -1747,7 +1747,7 @@
 qed "eps_split_left_le";
 
 Goal  (* eps_split_left_le_rev *)
-    "[|m le n; n le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|m le n; n le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)";
 by (rtac le_exists_lemma 1);
 by (REPEAT (assume_tac 1));
@@ -1756,7 +1756,7 @@
 qed "eps_split_left_le_rev";
 
 Goal  (* eps_split_right_le *)
-    "[|n le k; k le m; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|n le k; k le m; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)";
 by (rtac le_exists_lemma 1);
 by (REPEAT (assume_tac 1));
@@ -1765,7 +1765,7 @@
 qed "eps_split_right_le";
 
 Goal  (* eps_split_right_le_rev *)
-    "[|n le m; m le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|n le m; m le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)";
 by (rtac le_exists_lemma 1);
 by (REPEAT (assume_tac 1));
@@ -1776,7 +1776,7 @@
 (* The desired two theorems about `splitting'. *)
 
 Goal  (* eps_split_left *)
-    "[|m le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|m le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)";
 by (rtac nat_linear_le 1);
 by (rtac eps_split_right_le_rev 4);
@@ -1789,7 +1789,7 @@
 qed "eps_split_left";
 
 Goal  (* eps_split_right *)
-    "[|n le k; emb_chain(DD,ee); m:nat; n:nat; k:nat|] ==>  \
+    "[|n le k; emb_chain(DD,ee); m \\<in> nat; n \\<in> nat; k \\<in> nat|] ==>  \
 \    eps(DD,ee,m,n) = eps(DD,ee,k,n) O eps(DD,ee,m,k)";
 by (rtac nat_linear_le 1);
 by (rtac eps_split_left_le_rev 3);
@@ -1808,7 +1808,7 @@
 (* Considerably shorter. *)
 
 Goalw [rho_emb_def] (* rho_emb_fun *)
-    "[|emb_chain(DD,ee); n:nat|] ==>   \
+    "[|emb_chain(DD,ee); n \\<in> nat|] ==>   \
 \    rho_emb(DD,ee,n): set(DD`n) -> set(Dinf(DD,ee))";
 brr[lam_type, DinfI, eps_cont RS cont_fun RS apply_type] 1;
 by (Asm_simp_tac 1);
@@ -1838,23 +1838,23 @@
 qed "rho_emb_fun";
 
 Goalw [rho_emb_def]
-    "x:set(DD`n) ==> rho_emb(DD,ee,n)`x = (lam m:nat. eps(DD,ee,n,m)`x)";
+    "x \\<in> set(DD`n) ==> rho_emb(DD,ee,n)`x = (\\<lambda>m \\<in> nat. eps(DD,ee,n,m)`x)";
 by (Asm_simp_tac 1);
 qed "rho_emb_apply1";
 
 Goalw [rho_emb_def]
-    "[|x:set(DD`n); m:nat|] ==> rho_emb(DD,ee,n)`x`m = eps(DD,ee,n,m)`x";
+    "[|x \\<in> set(DD`n); m \\<in> nat|] ==> rho_emb(DD,ee,n)`x`m = eps(DD,ee,n,m)`x";
 by (Asm_simp_tac 1);
 qed "rho_emb_apply2";
 
-Goal "[| x:set(DD`n); n:nat|] ==> rho_emb(DD,ee,n)`x`n = x";
+Goal "[| x \\<in> set(DD`n); n \\<in> nat|] ==> rho_emb(DD,ee,n)`x`n = x";
 by (asm_simp_tac(simpset() addsimps[rho_emb_apply2,eps_id]) 1);
 qed "rho_emb_id";
 
 (* Shorter proof, 23 against 62. *)
 
 Goal (* rho_emb_cont *)
-    "[|emb_chain(DD,ee); n:nat|] ==>   \
+    "[|emb_chain(DD,ee); n \\<in> nat|] ==>   \
 \    rho_emb(DD,ee,n): cont(DD`n,Dinf(DD,ee))";
 by (rtac contI 1);
 brr[rho_emb_fun] 1;
@@ -1884,7 +1884,7 @@
 (* 32 vs 61, using safe_tac with imp in asm would be unfortunate (5steps) *)
 
 Goal (* lemma1 *)
-    "[|m le n; emb_chain(DD,ee); x:set(Dinf(DD,ee)); m:nat; n:nat|] ==>   \
+    "[|m le n; emb_chain(DD,ee); x \\<in> set(Dinf(DD,ee)); m \\<in> nat; n \\<in> nat|] ==>   \
 \    rel(DD`n,e_less(DD,ee,m,n)`(x`m),x`n)";
 by (etac rev_mp 1);  (* For induction proof *)
 by (induct_tac "n" 1);
@@ -1922,7 +1922,7 @@
 (* 18 vs 40 *)
 
 Goal (* lemma2 *)
-    "[|n le m; emb_chain(DD,ee); x:set(Dinf(DD,ee)); m:nat; n:nat|] ==>   \
+    "[|n le m; emb_chain(DD,ee); x \\<in> set(Dinf(DD,ee)); m \\<in> nat; n \\<in> nat|] ==>   \
 \    rel(DD`n,e_gr(DD,ee,m,n)`(x`m),x`n)";
 by (etac rev_mp 1);  (* For induction proof *)
 by (induct_tac "m" 1);
@@ -1944,7 +1944,7 @@
 val lemma2 = result();
 
 Goalw [eps_def] (* eps1 *)
-    "[|emb_chain(DD,ee); x:set(Dinf(DD,ee)); m:nat; n:nat|] ==>   \
+    "[|emb_chain(DD,ee); x \\<in> set(Dinf(DD,ee)); m \\<in> nat; n \\<in> nat|] ==>   \
 \    rel(DD`n,eps(DD,ee,m,n)`(x`m),x`n)";
 by (split_tac [split_if] 1);
 brr[conjI, impI, lemma1, not_le_iff_lt RS iffD1 RS leI RS lemma2, nat_into_Ord] 1;
@@ -1955,8 +1955,8 @@
    Look for occurences of rel_cfI, rel_DinfI, etc to evaluate the problem. *)
 
 Goal (* lam_Dinf_cont *)
-  "[| emb_chain(DD,ee); n:nat |] ==> \
-\  (lam x:set(Dinf(DD,ee)). x`n) : cont(Dinf(DD,ee),DD`n)";
+  "[| emb_chain(DD,ee); n \\<in> nat |] ==> \
+\  (\\<lambda>x \\<in> set(Dinf(DD,ee)). x`n) \\<in> cont(Dinf(DD,ee),DD`n)";
 by (rtac contI 1);
 brr[lam_type,apply_type,Dinf_prod] 1;
 by (Asm_simp_tac 1);
@@ -1967,7 +1967,7 @@
 qed "lam_Dinf_cont";
 
 Goalw  [rho_proj_def] (* rho_projpair *)
-    "[| emb_chain(DD,ee); n:nat |] ==> \
+    "[| emb_chain(DD,ee); n \\<in> nat |] ==> \
 \    projpair(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n),rho_proj(DD,ee,n))";
 by (rtac projpairI 1);
 brr[rho_emb_cont] 1;
@@ -1995,12 +1995,12 @@
 qed "rho_projpair";
 
 Goalw [emb_def]
-  "[| emb_chain(DD,ee); n:nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))";
+  "[| emb_chain(DD,ee); n \\<in> nat |] ==> emb(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))";
 by (auto_tac (claset() addIs [exI,rho_projpair], simpset()));
 qed "emb_rho_emb";
 
-Goal "[| emb_chain(DD,ee); n:nat |] ==>   \
-\  rho_proj(DD,ee,n) : cont(Dinf(DD,ee),DD`n)";
+Goal "[| emb_chain(DD,ee); n \\<in> nat |] ==>   \
+\  rho_proj(DD,ee,n) \\<in> cont(Dinf(DD,ee),DD`n)";
 by (auto_tac (claset() addIs [rho_projpair,projpair_p_cont], simpset()));
 qed "rho_proj_cont";
 
@@ -2009,22 +2009,22 @@
 (*----------------------------------------------------------------------*)
 
 val prems = Goalw [commute_def]  (* commuteI *)
-  "[| !!n. n:nat ==> emb(DD`n,E,r(n));   \
-\     !!m n. [|m le n; m:nat; n:nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |] ==>  \
+  "[| !!n. n \\<in> nat ==> emb(DD`n,E,r(n));   \
+\     !!m n. [|m le n; m \\<in> nat; n \\<in> nat|] ==> r(n) O eps(DD,ee,m,n) = r(m) |] ==>  \
 \  commute(DD,ee,E,r)";
 by Safe_tac;
 by (REPEAT (ares_tac prems 1));
 qed "commuteI";
 
 Goalw [commute_def]  (* commute_emb *)
-  "[| commute(DD,ee,E,r); n:nat |] ==> emb(DD`n,E,r(n))";
+  "[| commute(DD,ee,E,r); n \\<in> nat |] ==> emb(DD`n,E,r(n))";
 by (Fast_tac 1);
 qed "commute_emb";
 
 AddTCs [commute_emb];
 
 Goalw [commute_def]  (* commute_eq *)
-  "[| commute(DD,ee,E,r); m le n; m:nat; n:nat |] ==>   \
+  "[| commute(DD,ee,E,r); m le n; m \\<in> nat; n \\<in> nat |] ==>   \
 \  r(n) O eps(DD,ee,m,n) = r(m) ";
 by (Blast_tac 1);
 qed "commute_eq";
@@ -2046,7 +2046,7 @@
 by (auto_tac (claset() addIs [eps_fun], simpset()));
 qed "rho_emb_commute";
 
-val prems = goal Arith.thy "n:nat ==> n le succ(n)";
+val prems = goal Arith.thy "n \\<in> nat ==> n le succ(n)";
 by (REPEAT (ares_tac ((disjI1 RS(le_succ_iff RS iffD2))::le_refl::nat_into_Ord::prems) 1));
 qed "le_succ";
 
@@ -2054,7 +2054,7 @@
 
 Goal (* commute_chain *)
   "[| commute(DD,ee,E,r); emb_chain(DD,ee); cpo(E) |] ==>  \
-\  chain(cf(E,E),lam n:nat. r(n) O Rp(DD`n,E,r(n)))";
+\  chain(cf(E,E),\\<lambda>n \\<in> nat. r(n) O Rp(DD`n,E,r(n)))";
 by (rtac chainI 1);
 by (blast_tac (claset() addIs [lam_type, cont_cf, comp_pres_cont, commute_emb, Rp_cont, emb_cont, emb_chain_cpo]) 1);
 by (Asm_simp_tac 1);
@@ -2085,29 +2085,29 @@
 Goal (* rho_emb_chain *)
   "emb_chain(DD,ee) ==>  \
 \  chain(cf(Dinf(DD,ee),Dinf(DD,ee)),   \
-\        lam n:nat. rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))";
+\        \\<lambda>n \\<in> nat. rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))";
 by (auto_tac (claset() addIs [commute_chain,rho_emb_commute,cpo_Dinf], simpset()));
 qed "rho_emb_chain";
 
-Goal "[| emb_chain(DD,ee); x:set(Dinf(DD,ee)) |] ==>  \
+Goal "[| emb_chain(DD,ee); x \\<in> set(Dinf(DD,ee)) |] ==>  \
 \     chain(Dinf(DD,ee),   \
-\         lam n:nat.   \
+\         \\<lambda>n \\<in> nat.   \
 \          (rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))`x)";
 by (dtac (rho_emb_chain RS chain_cf) 1);
 by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 qed "rho_emb_chain_apply1";
 
-Goal "[| chain(iprod(DD),X); emb_chain(DD,ee); n:nat |] ==>  \
-\     chain(DD`n,lam m:nat. X `m `n)";
+Goal "[| chain(iprod(DD),X); emb_chain(DD,ee); n \\<in> nat |] ==>  \
+\     chain(DD`n,\\<lambda>m \\<in> nat. X `m `n)";
 by (auto_tac (claset() addIs [chain_iprod,emb_chain_cpo], simpset()));
 qed "chain_iprod_emb_chain";
 
 Goal (* rho_emb_chain_apply2 *)
-  "[| emb_chain(DD,ee); x:set(Dinf(DD,ee)); n:nat |] ==>  \
+  "[| emb_chain(DD,ee); x \\<in> set(Dinf(DD,ee)); n \\<in> nat |] ==>  \
 \  chain  \
 \   (DD`n,   \
-\    lam xa:nat.  \
+\    \\<lambda>xa \\<in> nat.  \
 \     (rho_emb(DD, ee, xa) O Rp(DD ` xa, Dinf(DD, ee),rho_emb(DD, ee, xa))) ` \
 \      x ` n)";
 by (forward_tac [rho_emb_chain_apply1 RS chain_Dinf RS chain_iprod_emb_chain] 1);
@@ -2119,7 +2119,7 @@
 Goal (* rho_emb_lub *)
   "emb_chain(DD,ee) ==>  \
 \  lub(cf(Dinf(DD,ee),Dinf(DD,ee)),   \
-\      lam n:nat. rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))) = \
+\      \\<lambda>n \\<in> nat. rho_emb(DD,ee,n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))) = \
 \  id(set(Dinf(DD,ee)))";
 by (rtac cpo_antisym 1);
 by (rtac cpo_cf 1); (* Instantiate variable, continued below (would loop otherwise) *)
@@ -2156,7 +2156,7 @@
 Goal (* theta_chain, almost same prf as commute_chain *)
   "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
 \     emb_chain(DD,ee); cpo(E); cpo(G) |] ==>  \
-\  chain(cf(E,G),lam n:nat. f(n) O Rp(DD`n,E,r(n)))";
+\  chain(cf(E,G),\\<lambda>n \\<in> nat. f(n) O Rp(DD`n,E,r(n)))";
 by (rtac chainI 1);
 by (blast_tac (claset() addIs [lam_type, cont_cf, comp_pres_cont, commute_emb, Rp_cont,emb_cont,emb_chain_cpo]) 1);
 by (Asm_simp_tac 1);
@@ -2182,7 +2182,7 @@
 Goal (* theta_proj_chain, same prf as theta_chain *)
   "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
 \     emb_chain(DD,ee); cpo(E); cpo(G) |] ==>  \
-\  chain(cf(G,E),lam n:nat. r(n) O Rp(DD`n,G,f(n)))";
+\  chain(cf(G,E),\\<lambda>n \\<in> nat. r(n) O Rp(DD`n,G,f(n)))";
 by (rtac chainI 1);
 by (blast_tac (claset() addIs [lam_type, cont_cf, comp_pres_cont, commute_emb, Rp_cont,emb_cont,emb_chain_cpo]) 1);
 by (Asm_simp_tac 1);
@@ -2205,7 +2205,7 @@
 			       emb_eps,le_succ]) 1));
 qed "theta_proj_chain";
 
-(* Simplification with comp_assoc is possible inside a lam-abstraction,
+(* Simplification with comp_assoc is possible inside a \\<lambda>-abstraction,
    because it does not have assumptions. If it had, as the HOL-ST theorem 
    too strongly has, we would be in deep trouble due to the lack of proper
    conditional rewriting (a HOL contrib provides something that works). *)
@@ -2213,7 +2213,7 @@
 (* Controlled simplification inside lambda: introduce lemmas *)
 
 Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
-\     emb_chain(DD,ee); cpo(E); cpo(G); x:nat |] ==>  \
+\     emb_chain(DD,ee); cpo(E); cpo(G); x \\<in> nat |] ==>  \
 \  r(x) O Rp(DD ` x, G, f(x)) O f(x) O Rp(DD ` x, E, r(x)) =  \
 \  r(x) O Rp(DD ` x, E, r(x))";
 by (res_inst_tac[("s1","f(x)")](comp_assoc RS subst) 1);
@@ -2227,13 +2227,13 @@
 (* Shorter proof (but lemmas): 19 vs 79 (103 - 24, due to OAssoc)  *)
 
 Goalw [projpair_def,rho_proj_def] (* theta_projpair *)
-  "[| lub(cf(E,E), lam n:nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));  \
+  "[| lub(cf(E,E), \\<lambda>n \\<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));  \
 \     commute(DD,ee,E,r); commute(DD,ee,G,f);   \
 \     emb_chain(DD,ee); cpo(E); cpo(G) |] ==>  \  
 \  projpair   \
 \   (E,G,   \
-\    lub(cf(E,G), lam n:nat. f(n) O Rp(DD`n,E,r(n))),  \
-\    lub(cf(G,E), lam n:nat. r(n) O Rp(DD`n,G,f(n))))";
+\    lub(cf(E,G), \\<lambda>n \\<in> nat. f(n) O Rp(DD`n,E,r(n))),  \
+\    lub(cf(G,E), \\<lambda>n \\<in> nat. r(n) O Rp(DD`n,G,f(n))))";
 by Safe_tac;
 by (stac comp_lubs 3);
 (* The following one line is 15 lines in HOL, and includes existentials. *)
@@ -2255,16 +2255,16 @@
 qed "theta_projpair";
 
 Goalw [emb_def]
-  "[| lub(cf(E,E), lam n:nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));  \
+  "[| lub(cf(E,E), \\<lambda>n \\<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));  \
 \     commute(DD,ee,E,r); commute(DD,ee,G,f);   \
 \     emb_chain(DD,ee); cpo(E); cpo(G) |] ==>  \  
-\  emb(E,G,lub(cf(E,G), lam n:nat. f(n) O Rp(DD`n,E,r(n))))";
+\  emb(E,G,lub(cf(E,G), \\<lambda>n \\<in> nat. f(n) O Rp(DD`n,E,r(n))))";
 by (blast_tac (claset() addIs [theta_projpair]) 1);
 qed "emb_theta";
 
 Goal (* mono_lemma *)
-  "[| g:cont(D,D'); cpo(D); cpo(D'); cpo(E) |] ==>  \
-\  (lam f : cont(D',E). f O g) : mono(cf(D',E),cf(D,E))";
+  "[| g \\<in> cont(D,D'); cpo(D); cpo(D'); cpo(E) |] ==>  \
+\  (\\<lambda>f \\<in> cont(D',E). f O g) \\<in> mono(cf(D',E),cf(D,E))";
 by (rtac monoI 1);
 by (REPEAT(dtac cf_cont 2));
 by (Asm_simp_tac 2);
@@ -2276,10 +2276,10 @@
 qed "mono_lemma";
 
 Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
-\        emb_chain(DD,ee); cpo(E); cpo(G); n:nat |] ==>  \  
-\     (lam na:nat. (lam f:cont(E, G). f O r(n)) `  \
-\      ((lam n:nat. f(n) O Rp(DD ` n, E, r(n))) ` na))  = \
-\     (lam na:nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))";
+\        emb_chain(DD,ee); cpo(E); cpo(G); n \\<in> nat |] ==>  \  
+\     (\\<lambda>na \\<in> nat. (\\<lambda>f \\<in> cont(E, G). f O r(n)) `  \
+\      ((\\<lambda>n \\<in> nat. f(n) O Rp(DD ` n, E, r(n))) ` na))  = \
+\     (\\<lambda>na \\<in> nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))";
 by (rtac fun_extension 1);
 by (fast_tac (claset() addIs [lam_type]) 1);
 by (Asm_simp_tac 2);
@@ -2287,8 +2287,8 @@
 val lemma = result();
 
 Goal "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
-\        emb_chain(DD,ee); cpo(E); cpo(G); n:nat |] ==>  \  
-\     chain(cf(DD`n,G),lam x:nat. (f(x) O Rp(DD ` x, E, r(x))) O r(n))";
+\        emb_chain(DD,ee); cpo(E); cpo(G); n \\<in> nat |] ==>  \  
+\     chain(cf(DD`n,G),\\<lambda>x \\<in> nat. (f(x) O Rp(DD ` x, E, r(x))) O r(n))";
 by (rtac (lemma RS subst) 1);
 by (REPEAT
     (blast_tac (claset() addIs[theta_chain,emb_chain_cpo,
@@ -2297,8 +2297,8 @@
 
 Goalw [suffix_def] (* suffix_lemma *)
   "[| commute(DD,ee,E,r); commute(DD,ee,G,f);   \
-\     emb_chain(DD,ee); cpo(E); cpo(G); cpo(DD`x); x:nat |] ==>  \  
-\  suffix(lam n:nat. (f(n) O Rp(DD`n,E,r(n))) O r(x),x) = (lam n:nat. f(x))";
+\     emb_chain(DD,ee); cpo(E); cpo(G); cpo(DD`x); x \\<in> nat |] ==>  \  
+\  suffix(\\<lambda>n \\<in> nat. (f(n) O Rp(DD`n,E,r(n))) O r(x),x) = (\\<lambda>n \\<in> nat. f(x))";
 by (Asm_simp_tac 1);
 by (rtac (lam_type RS fun_extension) 1); 
 by (REPEAT (blast_tac (claset() addIs [lam_type, comp_fun, cont_fun, Rp_cont, emb_cont, commute_emb, add_type,emb_chain_cpo]) 1));
@@ -2316,7 +2316,7 @@
 
 
 val prems = Goalw [mediating_def]
-  "[|emb(E,G,t);  !!n. n:nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)";
+  "[|emb(E,G,t);  !!n. n \\<in> nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)";
 by (Safe_tac);
 by (REPEAT (ares_tac prems 1));
 qed "mediatingI";
@@ -2325,15 +2325,15 @@
 by (Fast_tac 1);
 qed "mediating_emb";
 
-Goalw [mediating_def] "[| mediating(E,G,r,f,t); n:nat |] ==> f(n) = t O r(n)";
+Goalw [mediating_def] "[| mediating(E,G,r,f,t); n \\<in> nat |] ==> f(n) = t O r(n)";
 by (Blast_tac 1);
 qed "mediating_eq";
 
 Goal (* lub_universal_mediating *)
-  "[| lub(cf(E,E), lam n:nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));  \
+  "[| lub(cf(E,E), \\<lambda>n \\<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));  \
 \     commute(DD,ee,E,r); commute(DD,ee,G,f);   \
 \     emb_chain(DD,ee); cpo(E); cpo(G) |] ==>  \  
-\  mediating(E,G,r,f,lub(cf(E,G), lam n:nat. f(n) O Rp(DD`n,E,r(n))))";
+\  mediating(E,G,r,f,lub(cf(E,G), \\<lambda>n \\<in> nat. f(n) O Rp(DD`n,E,r(n))))";
 brr[mediatingI,emb_theta] 1;
 by (res_inst_tac[("b","r(n)")](lub_const RS subst) 1);
 by (stac comp_lubs 3);
@@ -2348,10 +2348,10 @@
 
 Goal (* lub_universal_unique *)
   "[| mediating(E,G,r,f,t);    \
-\     lub(cf(E,E), lam n:nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));   \
+\     lub(cf(E,E), \\<lambda>n \\<in> nat. r(n) O Rp(DD`n,E,r(n))) = id(set(E));   \
 \     commute(DD,ee,E,r); commute(DD,ee,G,f);   \
 \     emb_chain(DD,ee); cpo(E); cpo(G) |] ==>   \
-\  t = lub(cf(E,G), lam n:nat. f(n) O Rp(DD`n,E,r(n)))";
+\  t = lub(cf(E,G), \\<lambda>n \\<in> nat. f(n) O Rp(DD`n,E,r(n)))";
 by (res_inst_tac[("b","t")](comp_id RS subst) 1);
 by (etac subst 2);
 by (res_inst_tac[("b","t")](lub_const RS subst) 2);
@@ -2372,10 +2372,10 @@
 \  mediating   \
 \   (Dinf(DD,ee),G,rho_emb(DD,ee),f,   \
 \    lub(cf(Dinf(DD,ee),G),   \
-\        lam n:nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))) &  \
-\  (ALL t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) -->  \
+\        \\<lambda>n \\<in> nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n)))) &  \
+\  (\\<forall>t. mediating(Dinf(DD,ee),G,rho_emb(DD,ee),f,t) -->  \
 \    t = lub(cf(Dinf(DD,ee),G),   \
-\        lam n:nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))))";
+\        \\<lambda>n \\<in> nat. f(n) O Rp(DD`n,Dinf(DD,ee),rho_emb(DD,ee,n))))";
 by Safe_tac;
 brr[lub_universal_mediating,rho_emb_commute,rho_emb_lub,cpo_Dinf] 1;
 by (auto_tac (claset() addIs [lub_universal_unique,rho_emb_commute,rho_emb_lub,cpo_Dinf], simpset()));

--- a/src/ZF/ex/Limit.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Limit.thy	Mon May 21 14:36:24 2001 +0200
@@ -69,73 +69,73 @@
   
   po_def
     "po(D) ==   \
-\    (ALL x:set(D). rel(D,x,x)) &   \
-\    (ALL x:set(D). ALL y:set(D). ALL z:set(D).   \
+\    (\\<forall>x \\<in> set(D). rel(D,x,x)) &   \
+\    (\\<forall>x \\<in> set(D). \\<forall>y \\<in> set(D). \\<forall>z \\<in> set(D).   \
 \      rel(D,x,y) --> rel(D,y,z) --> rel(D,x,z)) &   \
-\    (ALL x:set(D). ALL y:set(D). rel(D,x,y) --> rel(D,y,x) --> x = y)"
+\    (\\<forall>x \\<in> set(D). \\<forall>y \\<in> set(D). rel(D,x,y) --> rel(D,y,x) --> x = y)"
 
     (* Chains are object level functions nat->set(D) *)
 
   chain_def
-    "chain(D,X) == X:nat->set(D) & (ALL n:nat. rel(D,X`n,X`(succ(n))))"
+    "chain(D,X) == X \\<in> nat->set(D) & (\\<forall>n \\<in> nat. rel(D,X`n,X`(succ(n))))"
 
   isub_def
-    "isub(D,X,x) == x:set(D) & (ALL n:nat. rel(D,X`n,x))"
+    "isub(D,X,x) == x \\<in> set(D) & (\\<forall>n \\<in> nat. rel(D,X`n,x))"
 
   islub_def
-    "islub(D,X,x) == isub(D,X,x) & (ALL y. isub(D,X,y) --> rel(D,x,y))"
+    "islub(D,X,x) == isub(D,X,x) & (\\<forall>y. isub(D,X,y) --> rel(D,x,y))"
 
   lub_def
     "lub(D,X) == THE x. islub(D,X,x)"
 
   cpo_def
-    "cpo(D) == po(D) & (ALL X. chain(D,X) --> (EX x. islub(D,X,x)))"
+    "cpo(D) == po(D) & (\\<forall>X. chain(D,X) --> (\\<exists>x. islub(D,X,x)))"
 
   pcpo_def
-    "pcpo(D) == cpo(D) & (EX x:set(D). ALL y:set(D). rel(D,x,y))"
+    "pcpo(D) == cpo(D) & (\\<exists>x \\<in> set(D). \\<forall>y \\<in> set(D). rel(D,x,y))"
   
   bot_def
-    "bot(D) == THE x. x:set(D) & (ALL y:set(D). rel(D,x,y))"
+    "bot(D) == THE x. x \\<in> set(D) & (\\<forall>y \\<in> set(D). rel(D,x,y))"
 
   
   mono_def
     "mono(D,E) ==   \
-\    {f:set(D)->set(E).   \
-\     ALL x:set(D). ALL y:set(D). rel(D,x,y) --> rel(E,f`x,f`y)}"
+\    {f \\<in> set(D)->set(E).   \
+\     \\<forall>x \\<in> set(D). \\<forall>y \\<in> set(D). rel(D,x,y) --> rel(E,f`x,f`y)}"
 
   cont_def
     "cont(D,E) ==   \
-\    {f:mono(D,E).   \
-\     ALL X. chain(D,X) --> f`(lub(D,X)) = lub(E,lam n:nat. f`(X`n))}" 
+\    {f \\<in> mono(D,E).   \
+\     \\<forall>X. chain(D,X) --> f`(lub(D,X)) = lub(E,\\<lambda>n \\<in> nat. f`(X`n))}" 
   
   cf_def
     "cf(D,E) ==   \
 \    <cont(D,E),   \
-\     {y:cont(D,E)*cont(D,E). ALL x:set(D). rel(E,(fst(y))`x,(snd(y))`x)}>"
+\     {y \\<in> cont(D,E)*cont(D,E). \\<forall>x \\<in> set(D). rel(E,(fst(y))`x,(snd(y))`x)}>"
 
   suffix_def
-    "suffix(X,n) == lam m:nat. X`(n #+ m)"
+    "suffix(X,n) == \\<lambda>m \\<in> nat. X`(n #+ m)"
 
   subchain_def
-    "subchain(X,Y) == ALL m:nat. EX n:nat. X`m = Y`(m #+ n)"
+    "subchain(X,Y) == \\<forall>m \\<in> nat. \\<exists>n \\<in> nat. X`m = Y`(m #+ n)"
 
   dominate_def
-    "dominate(D,X,Y) == ALL m:nat. EX n:nat. rel(D,X`m,Y`n)"
+    "dominate(D,X,Y) == \\<forall>m \\<in> nat. \\<exists>n \\<in> nat. rel(D,X`m,Y`n)"
 
   matrix_def
     "matrix(D,M) ==   \
-\    M: nat -> (nat -> set(D)) &   \
-\    (ALL n:nat. ALL m:nat. rel(D,M`n`m,M`succ(n)`m)) &   \
-\    (ALL n:nat. ALL m:nat. rel(D,M`n`m,M`n`succ(m))) &   \
-\    (ALL n:nat. ALL m:nat. rel(D,M`n`m,M`succ(n)`succ(m)))"
+\    M \\<in> nat -> (nat -> set(D)) &   \
+\    (\\<forall>n \\<in> nat. \\<forall>m \\<in> nat. rel(D,M`n`m,M`succ(n)`m)) &   \
+\    (\\<forall>n \\<in> nat. \\<forall>m \\<in> nat. rel(D,M`n`m,M`n`succ(m))) &   \
+\    (\\<forall>n \\<in> nat. \\<forall>m \\<in> nat. rel(D,M`n`m,M`succ(n)`succ(m)))"
 
   projpair_def
     "projpair(D,E,e,p) ==   \
-\    e:cont(D,E) & p:cont(E,D) &   \
+\    e \\<in> cont(D,E) & p \\<in> cont(E,D) &   \
 \    p O e = id(set(D)) & rel(cf(E,E),e O p,id(set(E)))"
 
   emb_def
-    "emb(D,E,e) == EX p. projpair(D,E,e,p)"
+    "emb(D,E,e) == \\<exists>p. projpair(D,E,e,p)"
 
   Rp_def
     "Rp(D,E,e) == THE p. projpair(D,E,e,p)"
@@ -144,32 +144,32 @@
 
   iprod_def
     "iprod(DD) ==   \
-\    <(PROD n:nat. set(DD`n)),  \
-\     {x:(PROD n:nat. set(DD`n))*(PROD n:nat. set(DD`n)).   \
-\      ALL n:nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"
+\    <(\\<Pi>n \\<in> nat. set(DD`n)),  \
+\     {x:(\\<Pi>n \\<in> nat. set(DD`n))*(\\<Pi>n \\<in> nat. set(DD`n)).   \
+\      \\<forall>n \\<in> nat. rel(DD`n,fst(x)`n,snd(x)`n)}>"
 
   mkcpo_def   (* Cannot use rel(D), is meta fun, need two more args *)
     "mkcpo(D,P) ==   \
-\    <{x:set(D). P(x)},{x:set(D)*set(D). rel(D,fst(x),snd(x))}>"
+\    <{x \\<in> set(D). P(x)},{x \\<in> set(D)*set(D). rel(D,fst(x),snd(x))}>"
 
 
   subcpo_def
     "subcpo(D,E) ==   \
-\    set(D) <= set(E) &   \
-\    (ALL x:set(D). ALL y:set(D). rel(D,x,y) <-> rel(E,x,y)) &   \
-\    (ALL X. chain(D,X) --> lub(E,X):set(D))"
+\    set(D) \\<subseteq> set(E) &   \
+\    (\\<forall>x \\<in> set(D). \\<forall>y \\<in> set(D). rel(D,x,y) <-> rel(E,x,y)) &   \
+\    (\\<forall>X. chain(D,X) --> lub(E,X):set(D))"
 
   subpcpo_def
     "subpcpo(D,E) == subcpo(D,E) & bot(E):set(D)"
 
   emb_chain_def
     "emb_chain(DD,ee) ==   \
-\    (ALL n:nat. cpo(DD`n)) & (ALL n:nat. emb(DD`n,DD`succ(n),ee`n))"
+\    (\\<forall>n \\<in> nat. cpo(DD`n)) & (\\<forall>n \\<in> nat. emb(DD`n,DD`succ(n),ee`n))"
 
   Dinf_def
     "Dinf(DD,ee) ==   \
 \    mkcpo(iprod(DD))   \
-\    (%x. ALL n:nat. Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n)"
+\    (%x. \\<forall>n \\<in> nat. Rp(DD`n,DD`succ(n),ee`n)`(x`succ(n)) = x`n)"
 
   e_less_def (* Valid for m le n only. *)
     "e_less(DD,ee,m,n) == rec(n#-m,id(set(DD`m)),%x y. ee`(m#+x) O y)"
@@ -183,17 +183,17 @@
     "eps(DD,ee,m,n) == if(m le n,e_less(DD,ee,m,n),e_gr(DD,ee,m,n))"
 
   rho_emb_def
-    "rho_emb(DD,ee,n) == lam x:set(DD`n). lam m:nat. eps(DD,ee,n,m)`x"
+    "rho_emb(DD,ee,n) == \\<lambda>x \\<in> set(DD`n). \\<lambda>m \\<in> nat. eps(DD,ee,n,m)`x"
 
   rho_proj_def
-    "rho_proj(DD,ee,n) == lam x:set(Dinf(DD,ee)). x`n"
+    "rho_proj(DD,ee,n) == \\<lambda>x \\<in> set(Dinf(DD,ee)). x`n"
   
   commute_def
     "commute(DD,ee,E,r) ==   \
-\    (ALL n:nat. emb(DD`n,E,r(n))) &   \
-\    (ALL m:nat. ALL n:nat. m le n --> r(n) O eps(DD,ee,m,n) = r(m))"
+\    (\\<forall>n \\<in> nat. emb(DD`n,E,r(n))) &   \
+\    (\\<forall>m \\<in> nat. \\<forall>n \\<in> nat. m le n --> r(n) O eps(DD,ee,m,n) = r(m))"
 
   mediating_def
-    "mediating(E,G,r,f,t) == emb(E,G,t) & (ALL n:nat. f(n) = t O r(n))"
+    "mediating(E,G,r,f,t) == emb(E,G,t) & (\\<forall>n \\<in> nat. f(n) = t O r(n))"
 
 end

--- a/src/ZF/ex/ListN.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/ListN.ML	Mon May 21 14:36:24 2001 +0200
@@ -9,38 +9,38 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-Goal "l:list(A) ==> <length(l),l> : listn(A)";
+Goal "l \\<in> list(A) ==> <length(l),l> \\<in> listn(A)";
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (REPEAT (ares_tac listn.intrs 1));
 qed "list_into_listn";
 
-Goal "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
+Goal "<n,l> \\<in> listn(A) <-> l \\<in> list(A) & length(l)=n";
 by (rtac iffI 1);
 by (blast_tac (claset() addIs [list_into_listn]) 2);
 by (etac listn.induct 1);
 by Auto_tac;
 qed "listn_iff";
 
-Goal "listn(A)``{n} = {l:list(A). length(l)=n}";
+Goal "listn(A)``{n} = {l \\<in> list(A). length(l)=n}";
 by (rtac equality_iffI 1);
 by (simp_tac (simpset() addsimps [listn_iff,separation,image_singleton_iff]) 1);
 qed "listn_image_eq";
 
-Goalw listn.defs "A<=B ==> listn(A) <= listn(B)";
+Goalw listn.defs "A \\<subseteq> B ==> listn(A) \\<subseteq> listn(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac listn.bnd_mono 1));
 by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
 qed "listn_mono";
 
-Goal "[| <n,l> : listn(A); <n',l'> : listn(A) |] ==> <n#+n', l@l'> : listn(A)";
+Goal "[| <n,l> \\<in> listn(A); <n',l'> \\<in> listn(A) |] ==> <n#+n', l@l'> \\<in> listn(A)";
 by (etac listn.induct 1);
 by (ftac (impOfSubs listn.dom_subset) 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps listn.intrs)));
 qed "listn_append";
 
-val Nil_listn_case  = listn.mk_cases "<i,Nil> : listn(A)"
-and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> : listn(A)";
+val Nil_listn_case  = listn.mk_cases "<i,Nil> \\<in> listn(A)"
+and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> \\<in> listn(A)";
 
-val zero_listn_case = listn.mk_cases "<0,l> : listn(A)"
-and succ_listn_case = listn.mk_cases "<succ(i),l> : listn(A)";
+val zero_listn_case = listn.mk_cases "<0,l> \\<in> listn(A)"
+and succ_listn_case = listn.mk_cases "<succ(i),l> \\<in> listn(A)";

--- a/src/ZF/ex/ListN.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/ListN.thy	Mon May 21 14:36:24 2001 +0200
@@ -14,7 +14,7 @@
 inductive
   domains   "listn(A)" <= "nat*list(A)"
   intrs
-    NilI  "<0,Nil> : listn(A)"
-    ConsI "[| a: A;  <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
+    NilI  "<0,Nil> \\<in> listn(A)"
+    ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)"
   type_intrs "nat_typechecks @ list.intrs"
 end

--- a/src/ZF/ex/Mutil.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Mutil.ML	Mon May 21 14:36:24 2001 +0200
@@ -15,7 +15,7 @@
 by (Blast_tac 1);
 qed "evnodd_iff";
 
-Goalw [evnodd_def] "evnodd(A, b) <= A";
+Goalw [evnodd_def] "evnodd(A, b) \\<subseteq> A";
 by (Blast_tac 1);
 qed "evnodd_subset";
 
@@ -44,11 +44,11 @@
 
 (*** Dominoes ***)
 
-Goal "d:domino ==> Finite(d)";
+Goal "d \\<in> domino ==> Finite(d)";
 by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1);
 qed "domino_Finite";
 
-Goal "[| d:domino; b<2 |] ==> EX i' j'. evnodd(d,b) = {<i',j'>}";
+Goal "[| d \\<in> domino; b<2 |] ==> \\<exists>i' j'. evnodd(d,b) = {<i',j'>}";
 by (eresolve_tac [domino.elim] 1);
 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 2);
 by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 1);
@@ -63,8 +63,8 @@
 
 (** The union of two disjoint tilings is a tiling **)
 
-Goal "t: tiling(A) ==> \
-\              u: tiling(A) --> t Int u = 0 --> t Un u : tiling(A)";
+Goal "t \\<in> tiling(A) ==> \
+\              u \\<in> tiling(A) --> t Int u = 0 --> t Un u \\<in> tiling(A)";
 by (etac tiling.induct 1);
 by (simp_tac (simpset() addsimps tiling.intrs) 1);
 by (asm_full_simp_tac (simpset() addsimps [Un_assoc,
@@ -72,13 +72,13 @@
 by (blast_tac (claset() addIs tiling.intrs) 1);
 qed_spec_mp "tiling_UnI";
 
-Goal "t:tiling(domino) ==> Finite(t)";
+Goal "t \\<in> tiling(domino) ==> Finite(t)";
 by (eresolve_tac [tiling.induct] 1);
 by (rtac Finite_0 1);
 by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1);
 qed "tiling_domino_Finite";
 
-Goal "t: tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|";
+Goal "t \\<in> tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|";
 by (eresolve_tac [tiling.induct] 1);
 by (simp_tac (simpset() addsimps [evnodd_def]) 1);
 by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
@@ -86,7 +86,7 @@
 by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
 by (Simp_tac 2 THEN assume_tac 1);
 by Safe_tac;
-by (subgoal_tac "ALL p b. p:evnodd(a,b) --> p~:evnodd(t,b)" 1);
+by (subgoal_tac "\\<forall>p b. p \\<in> evnodd(a,b) --> p\\<notin>evnodd(t,b)" 1);
 by (asm_simp_tac 
     (simpset() addsimps [evnodd_Un, Un_cons, tiling_domino_Finite,
 			 evnodd_subset RS subset_Finite,
@@ -95,7 +95,7 @@
                         addEs [equalityE]) 1);
 qed "tiling_domino_0_1";
 
-Goal "[| i: nat;  n: nat |] ==> {i} * (n #+ n) : tiling(domino)";
+Goal "[| i \\<in> nat;  n \\<in> nat |] ==> {i} * (n #+ n) \\<in> tiling(domino)";
 by (induct_tac "n" 1);
 by (simp_tac (simpset() addsimps tiling.intrs) 1);
 by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1);
@@ -109,7 +109,7 @@
 by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1);
 qed "dominoes_tile_row";
 
-Goal "[| m: nat;  n: nat |] ==> m * (n #+ n) : tiling(domino)";
+Goal "[| m \\<in> nat;  n \\<in> nat |] ==> m * (n #+ n) \\<in> tiling(domino)";
 by (induct_tac "m" 1);
 by (simp_tac (simpset() addsimps tiling.intrs) 1);
 by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1);
@@ -121,14 +121,14 @@
 by Auto_tac;
 qed "eq_lt_E";
 
-Goal "[| m: nat;  n: nat;                                 \
+Goal "[| m \\<in> nat;  n \\<in> nat;                                 \
 \        t = (succ(m)#+succ(m))*(succ(n)#+succ(n));       \
 \        t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] \
-\     ==> t' ~: tiling(domino)";
+\     ==> t' \\<notin> tiling(domino)";
 by (rtac notI 1);
 by (dtac tiling_domino_0_1 1);
 by (eres_inst_tac [("x", "|?A|")] eq_lt_E 1);
-by (subgoal_tac "t : tiling(domino)" 1);
+by (subgoal_tac "t \\<in> tiling(domino)" 1);
 (*Requires a small simpset that won't move the succ applications*)
 by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, 
                                   dominoes_tile_matrix]) 2);

--- a/src/ZF/ex/Mutil.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Mutil.thy	Mon May 21 14:36:24 2001 +0200
@@ -16,21 +16,21 @@
 inductive
   domains "domino" <= "Pow(nat*nat)"
   intrs
-    horiz  "[| i: nat;  j: nat |] ==> {<i,j>, <i,succ(j)>} : domino"
-    vertl  "[| i: nat;  j: nat |] ==> {<i,j>, <succ(i),j>} : domino"
+    horiz  "[| i \\<in> nat;  j \\<in> nat |] ==> {<i,j>, <i,succ(j)>} \\<in> domino"
+    vertl  "[| i \\<in> nat;  j \\<in> nat |] ==> {<i,j>, <succ(i),j>} \\<in> domino"
   type_intrs  empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI
 
 
 inductive
     domains "tiling(A)" <= "Pow(Union(A))"
   intrs
-    empty  "0 : tiling(A)"
-    Un     "[| a: A;  t: tiling(A);  a Int t = 0 |] ==> a Un t : tiling(A)"
+    empty  "0 \\<in> tiling(A)"
+    Un     "[| a \\<in> A;  t \\<in> tiling(A);  a Int t = 0 |] ==> a Un t \\<in> tiling(A)"
   type_intrs  empty_subsetI, Union_upper, Un_least, PowI
   type_elims "[make_elim PowD]"
 
 constdefs
   evnodd  :: [i,i]=>i
-  "evnodd(A,b) == {z:A. EX i j. z=<i,j> & (i#+j) mod 2 = b}"
+  "evnodd(A,b) == {z \\<in> A. \\<exists>i j. z=<i,j> & (i#+j) mod 2 = b}"
 
 end

--- a/src/ZF/ex/NatSum.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/NatSum.ML	Mon May 21 14:36:24 2001 +0200
@@ -15,20 +15,20 @@
 Addsimps [zdiff_zmult_distrib, zdiff_zmult_distrib2];
 
 (*The sum of the first n odd numbers equals n squared.*)
-Goal "n: nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
+Goal "n \\<in> nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_odds";
 
 (*The sum of the first n odd squares*)
-Goal "n: nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
+Goal "n \\<in> nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
 \     $#n $* (#4 $* $#n $* $#n $- #1)";
 by (induct_tac "n" 1);
 by Auto_tac;  
 qed "sum_of_odd_squares";
 
 (*The sum of the first n odd cubes*)
-Goal "n: nat \
+Goal "n \\<in> nat \
 \     ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
 \         $#n $* $#n $* (#2 $* $#n $* $#n $- #1)";
 by (induct_tac "n" 1);
@@ -36,18 +36,18 @@
 qed "sum_of_odd_cubes";
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
-Goal "n: nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
+Goal "n \\<in> nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_naturals";
 
-Goal "n: nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
+Goal "n \\<in> nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
 \                $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "sum_of_squares";
 
-Goal "n: nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
+Goal "n \\<in> nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
 \                $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)";
 by (induct_tac "n" 1);
 by Auto_tac;
@@ -55,7 +55,7 @@
 
 (** Sum of fourth powers **)
 
-Goal "n: nat ==> \
+Goal "n \\<in> nat ==> \
 \     #30 $* sum (%i. i$*i$*i$*i, succ(n)) = \
 \     $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* \
 \     (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)";

--- a/src/ZF/ex/Ntree.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Ntree.ML	Mon May 21 14:36:24 2001 +0200
@@ -11,7 +11,7 @@
 
 (** ntree **)
 
-Goal "ntree(A) = A * (UN n: nat. n -> ntree(A))";
+Goal "ntree(A) = A * (\\<Union>n \\<in> nat. n -> ntree(A))";
 let open ntree;  val rew = rewrite_rule con_defs in  
 by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
 end;
@@ -19,8 +19,8 @@
 
 (*A nicer induction rule than the standard one*)
 val major::prems = goal Ntree.thy
-    "[| t: ntree(A);                                                    \
-\       !!x n h. [| x: A;  n: nat;  h: n -> ntree(A);  ALL i:n. P(h`i)  \
+    "[| t \\<in> ntree(A);                                                    \
+\       !!x n h. [| x \\<in> A;  n \\<in> nat;  h \\<in> n -> ntree(A);  \\<forall>i \\<in> n. P(h`i)  \
 \                |] ==> P(Branch(x,h))                                  \
 \    |] ==> P(t)";
 by (rtac (major RS ntree.induct) 1);
@@ -32,8 +32,8 @@
 
 (*Induction on ntree(A) to prove an equation*)
 val major::prems = goal Ntree.thy
-  "[| t: ntree(A);  f: ntree(A)->B;  g: ntree(A)->B;                      \
-\     !!x n h. [| x: A;  n: nat;  h: n -> ntree(A);  f O h = g O h |] ==> \
+  "[| t \\<in> ntree(A);  f \\<in> ntree(A)->B;  g \\<in> ntree(A)->B;                      \
+\     !!x n h. [| x \\<in> A;  n \\<in> nat;  h \\<in> n -> ntree(A);  f O h = g O h |] ==> \
 \              f ` Branch(x,h) = g ` Branch(x,h)                          \
 \  |] ==> f`t=g`t";
 by (rtac (major RS ntree_induct) 1);
@@ -46,14 +46,14 @@
 
 (**  Lemmas to justify using "Ntree" in other recursive type definitions **)
 
-Goalw ntree.defs "A<=B ==> ntree(A) <= ntree(B)";
+Goalw ntree.defs "A \\<subseteq> B ==> ntree(A) \\<subseteq> ntree(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac ntree.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
 qed "ntree_mono";
 
 (*Easily provable by induction also*)
-Goalw (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)";
+Goalw (ntree.defs@ntree.con_defs) "ntree(univ(A)) \\<subseteq> univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac (A_subset_univ RS univ_mono) 2);
 by Safe_tac;
@@ -66,7 +66,7 @@
 (** ntree recursion **)
 
 Goal "ntree_rec(b, Branch(x,h)) \
-\     = b(x, h, lam i: domain(h). ntree_rec(b, h`i))";
+\     = b(x, h, \\<lambda>i \\<in> domain(h). ntree_rec(b, h`i))";
 by (rtac (ntree_rec_def RS def_Vrecursor RS trans) 1);
 by (Simp_tac 1);
 by (rewrite_goals_tac ntree.con_defs);
@@ -75,13 +75,13 @@
 qed "ntree_rec_Branch";
 
 Goalw [ntree_copy_def]
- "ntree_copy (Branch(x, h)) = Branch(x, lam i : domain(h). ntree_copy (h`i))";
+ "ntree_copy (Branch(x, h)) = Branch(x, \\<lambda>i \\<in> domain(h). ntree_copy (h`i))";
 by (rtac ntree_rec_Branch 1);
 qed "ntree_copy_Branch";
 
 Addsimps [ntree_copy_Branch];
 
-Goal "z : ntree(A) ==> ntree_copy(z) = z";
+Goal "z \\<in> ntree(A) ==> ntree_copy(z) = z";
 by (induct_tac "z" 1);
 by (auto_tac (claset(), simpset() addsimps [domain_of_fun, Pi_Collect_iff]));
 qed "ntree_copy_is_ident";
@@ -98,9 +98,9 @@
 
 (*A nicer induction rule than the standard one*)
 val major::prems = goal Ntree.thy
-    "[| t: maptree(A);                                                  \
-\       !!x n h. [| x: A;  h: maptree(A) -||> maptree(A);               \
-\                   ALL y: field(h). P(y)                               \
+    "[| t \\<in> maptree(A);                                                  \
+\       !!x n h. [| x \\<in> A;  h \\<in> maptree(A) -||> maptree(A);               \
+\                   \\<forall>y \\<in> field(h). P(y)                               \
 \                |] ==> P(Sons(x,h))                                    \
 \    |] ==> P(t)";
 by (rtac (major RS maptree.induct) 1);
@@ -122,8 +122,8 @@
 
 (*A nicer induction rule than the standard one*)
 val major::prems = goal Ntree.thy
-    "[| t: maptree2(A,B);                                                 \
-\       !!x n h. [| x: A;  h: B -||> maptree2(A,B);  ALL y:range(h). P(y) \
+    "[| t \\<in> maptree2(A,B);                                                 \
+\       !!x n h. [| x \\<in> A;  h \\<in> B -||> maptree2(A,B);  \\<forall>y \\<in> range(h). P(y) \
 \                |] ==> P(Sons2(x,h))                                     \
 \    |] ==> P(t)";
 by (rtac (major RS maptree2.induct) 1);

--- a/src/ZF/ex/Ntree.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Ntree.thy	Mon May 21 14:36:24 2001 +0200
@@ -16,18 +16,18 @@
   maptree2 :: [i,i] => i
 
 datatype
-  "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
+  "ntree(A)" = Branch ("a \\<in> A", "h \\<in> (\\<Union>n \\<in> nat. n -> ntree(A))")
   monos       "[[subset_refl, Pi_mono] MRS UN_mono]"    (*MUST have this form*)
   type_intrs  "[nat_fun_univ RS subsetD]"
   type_elims   UN_E
 
 datatype
-  "maptree(A)" = Sons ("a: A", "h: maptree(A) -||> maptree(A)")
+  "maptree(A)" = Sons ("a \\<in> A", "h \\<in> maptree(A) -||> maptree(A)")
   monos        FiniteFun_mono1         (*Use monotonicity in BOTH args*)
   type_intrs  "[FiniteFun_univ1 RS subsetD]"
 
 datatype
-  "maptree2(A,B)" = Sons2 ("a: A", "h: B -||> maptree2(A,B)")
+  "maptree2(A,B)" = Sons2 ("a \\<in> A", "h \\<in> B -||> maptree2(A,B)")
   monos       "[subset_refl RS FiniteFun_mono]"
   type_intrs   FiniteFun_in_univ'
 
@@ -35,7 +35,7 @@
 constdefs
   ntree_rec  :: [[i,i,i]=>i, i] => i
    "ntree_rec(b) == 
-    Vrecursor(%pr. ntree_case(%x h. b(x, h, lam i: domain(h). pr`(h`i))))"
+    Vrecursor(%pr. ntree_case(%x h. b(x, h, \\<lambda>i \\<in> domain(h). pr`(h`i))))"
 
 constdefs
     ntree_copy     :: i=>i

--- a/src/ZF/ex/Primes.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Primes.ML	Mon May 21 14:36:24 2001 +0200
@@ -12,7 +12,7 @@
 (** Divides Relation                           **)
 (************************************************)
 
-Goalw [dvd_def] "m dvd n ==> m:nat & n:nat & (EX k:nat. n = m#*k)";
+Goalw [dvd_def] "m dvd n ==> m \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)";
 by (assume_tac 1);
 qed "dvdD";
 
@@ -20,7 +20,7 @@
 bind_thm ("dvd_imp_nat2", dvdD RS conjunct2 RS conjunct1);
 
 
-Goalw [dvd_def] "m:nat ==> m dvd 0";
+Goalw [dvd_def] "m \\<in> nat ==> m dvd 0";
 by (fast_tac (claset() addIs [nat_0I, mult_0_right RS sym]) 1);
 qed "dvd_0_right";
 
@@ -28,7 +28,7 @@
 by (fast_tac (claset() addss (simpset())) 1);
 qed "dvd_0_left";
 
-Goalw [dvd_def] "m:nat ==> m dvd m";
+Goalw [dvd_def] "m \\<in> nat ==> m dvd m";
 by (fast_tac (claset() addIs [nat_1I, mult_1_right RS sym]) 1);
 qed "dvd_refl";
 
@@ -48,23 +48,23 @@
 
 (* GCD by Euclid's Algorithm *)
 
-Goalw [egcd_def] "m:nat ==> egcd(m,0) = m";
+Goalw [egcd_def] "m \\<in> nat ==> egcd(m,0) = m";
 by (stac transrec 1);
 by (Asm_simp_tac 1);
 qed "egcd_0";
 
 Goalw [egcd_def]
-    "[| 0<n; m:nat; n:nat |] ==> egcd(m,n) = egcd(n, m mod n)";
+    "[| 0<n; m \\<in> nat; n \\<in> nat |] ==> egcd(m,n) = egcd(n, m mod n)";
 by (res_inst_tac [("P", "%z. ?left(z) = ?right")] (transrec RS ssubst) 1);
 by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq RS not_sym,
                                      mod_less_divisor RS ltD]) 1);
 qed "egcd_lt_0";
 
-Goal "m:nat ==> egcd(m,0) dvd m";
+Goal "m \\<in> nat ==> egcd(m,0) dvd m";
 by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl]) 1);
 qed "egcd_0_dvd_m";
 
-Goal "m:nat ==> egcd(m,0) dvd 0";
+Goal "m \\<in> nat ==> egcd(m,0) dvd 0";
 by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_0_right]) 1);
 qed "egcd_0_dvd_0";
 
@@ -72,11 +72,11 @@
 by (fast_tac (claset() addIs [add_mult_distrib_left RS sym, add_type]) 1);
 qed "dvd_add";
 
-Goalw [dvd_def] "[| k dvd a; q:nat |] ==> k dvd (q #* a)";
+Goalw [dvd_def] "[| k dvd a; q \\<in> nat |] ==> k dvd (q #* a)";
 by (fast_tac (claset() addIs [mult_left_commute, mult_type]) 1);
 qed "dvd_mult";
 
-Goal "[| k dvd b; k dvd (a mod b); 0 < b; a:nat |] ==> k dvd a";
+Goal "[| k dvd b; k dvd (a mod b); 0 < b; a \\<in> nat |] ==> k dvd a";
 by (deepen_tac 
     (claset() addIs [mod_div_equality RS subst]
            addDs [dvdD]
@@ -86,7 +86,7 @@
 
 (* egcd type *)
 
-Goal "b:nat ==> ALL a:nat. egcd(a,b):nat";
+Goal "b \\<in> nat ==> \\<forall>a \\<in> nat. egcd(a,b):nat";
 by (etac complete_induct 1);
 by (rtac ballI 1);
 by (excluded_middle_tac "x=0" 1);
@@ -103,7 +103,7 @@
 
 (* Property 1: egcd(a,b) divides a and b *)
 
-Goal "b:nat ==> ALL a: nat. (egcd(a,b) dvd a) & (egcd(a,b) dvd b)";
+Goal "b \\<in> nat ==> \\<forall>a \\<in> nat. (egcd(a,b) dvd a) & (egcd(a,b) dvd b)";
 by (res_inst_tac [("i","b")] complete_induct 1);
 by (assume_tac 1);
 by (rtac ballI 1);
@@ -138,8 +138,8 @@
 
 (* Property 2: for all a,b,f naturals, 
                if f divides a and f divides b then f divides egcd(a,b)*)
-Goal "[| b:nat; f:nat |] ==>    \
-\              ALL a. (f dvd a) & (f dvd b) --> f dvd egcd(a,b)";
+Goal "[| b \\<in> nat; f \\<in> nat |] ==>    \
+\              \\<forall>a. (f dvd a) & (f dvd b) --> f dvd egcd(a,b)";
 by (etac complete_induct 1);
 by (rtac allI 1);
 by (excluded_middle_tac "x=0" 1);
@@ -157,9 +157,9 @@
 by (fast_tac (claset() addSIs [dvd_mod, nat_into_Ord RS Ord_0_lt]) 1);
 qed "egcd_prop2";
 
-(* GCD PROOF : GCD exists and egcd fits the definition *)
+(* GCD PROOF \\<in> GCD exists and egcd fits the definition *)
 
-Goalw [gcd_def] "[| a: nat; b:nat |] ==> gcd(egcd(a,b), a, b)";
+Goalw [gcd_def] "[| a \\<in> nat; b \\<in> nat |] ==> gcd(egcd(a,b), a, b)";
 by (asm_simp_tac (simpset() addsimps [egcd_prop1]) 1);
 by (fast_tac (claset() addIs [egcd_prop2 RS spec RS mp, dvd_imp_nat1]) 1);
 qed "gcd";

--- a/src/ZF/ex/Primes.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Primes.thy	Mon May 21 14:36:24 2001 +0200
@@ -15,16 +15,16 @@
   prime   :: i=>o                  (* prime definition *)
   
 defs
-  dvd_def     "m dvd n == m:nat & n:nat & (EX k:nat. n = m#*k)"
+  dvd_def     "m dvd n == m \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)"
 
   gcd_def     "gcd(p,m,n) == ((p dvd m) & (p dvd n))   &
-               (ALL d. (d dvd m) & (d dvd n) --> d dvd p)"
+               (\\<forall>d. (d dvd m) & (d dvd n) --> d dvd p)"
 
   egcd_def    "egcd(m,n) ==   
-               transrec(n, %n f. lam m:nat. if(n=0, m, f`(m mod n)`n)) ` m"
+               transrec(n, %n f. \\<lambda>m \\<in> nat. if(n=0, m, f`(m mod n)`n)) ` m"
 
   coprime_def "coprime(m,n) == egcd(m,n) = 1"
 
-  prime_def   "prime(n) == (1<n) & (ALL m:nat. 1<m & m<n --> ~(m dvd n))"
+  prime_def   "prime(n) == (1<n) & (\\<forall>m \\<in> nat. 1<m & m<n --> ~(m dvd n))"
 
 end

--- a/src/ZF/ex/Primrec.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Primrec.ML	Mon May 21 14:36:24 2001 +0200
@@ -16,12 +16,12 @@
 
 (*** Inductive definition of the PR functions ***)
 
-(* c: prim_rec ==> c: list(nat) -> nat *)
+(* c \\<in> prim_rec ==> c \\<in> list(nat) -> nat *)
 val prim_rec_into_fun = prim_rec.dom_subset RS subsetD;
 
 AddTCs ([prim_rec_into_fun] @ prim_rec.intrs);
 
-Goal "i:nat ==> ACK(i): prim_rec";
+Goal "i \\<in> nat ==> ACK(i): prim_rec";
 by (induct_tac "i" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "ACK_in_prim_rec";
@@ -29,7 +29,7 @@
 AddTCs [ACK_in_prim_rec, prim_rec_into_fun RS apply_type,
 	list_add_type, nat_into_Ord, rec_type];
 
-Goal "[| i:nat;  j:nat |] ==>  ack(i,j): nat";
+Goal "[| i \\<in> nat;  j \\<in> nat |] ==>  ack(i,j): nat";
 by Auto_tac;
 qed "ack_type";
 AddTCs [ack_type];
@@ -37,7 +37,7 @@
 (** Ackermann's function cases **)
 
 (*PROPERTY A 1*)
-Goal "j:nat ==> ack(0,j) = succ(j)";
+Goal "j \\<in> nat ==> ack(0,j) = succ(j)";
 by (asm_simp_tac (simpset() addsimps [SC]) 1);
 qed "ack_0";
 
@@ -47,7 +47,7 @@
 qed "ack_succ_0";
 
 (*PROPERTY A 3*)
-Goal "[| i:nat;  j:nat |]  \
+Goal "[| i \\<in> nat;  j \\<in> nat |]  \
 \     ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
 by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
 qed "ack_succ_succ";
@@ -57,7 +57,7 @@
 
 
 (*PROPERTY A 4*)
-Goal "i:nat ==> ALL j:nat. j < ack(i,j)";
+Goal "i \\<in> nat ==> \\<forall>j \\<in> nat. j < ack(i,j)";
 by (induct_tac "i" 1);
 by (Asm_simp_tac 1);
 by (rtac ballI 1);
@@ -68,13 +68,13 @@
 qed_spec_mp "lt_ack2";
 
 (*PROPERTY A 5-, the single-step lemma*)
-Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
+Goal "[| i \\<in> nat; j \\<in> nat |] ==> ack(i,j) < ack(i, succ(j))";
 by (induct_tac "i" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack2])));
 qed "ack_lt_ack_succ2";
 
 (*PROPERTY A 5, monotonicity for < *)
-Goal "[| j<k; i:nat; k:nat |] ==> ack(i,j) < ack(i,k)";
+Goal "[| j<k; i \\<in> nat; k \\<in> nat |] ==> ack(i,j) < ack(i,k)";
 by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
 by (etac succ_lt_induct 1);
 by (assume_tac 1);
@@ -83,13 +83,13 @@
 qed "ack_lt_mono2";
 
 (*PROPERTY A 5', monotonicity for le *)
-Goal "[| j le k;  i: nat;  k:nat |] ==> ack(i,j) le ack(i,k)";
+Goal "[| j le k;  i \\<in> nat;  k \\<in> nat |] ==> ack(i,j) le ack(i,k)";
 by (res_inst_tac [("f", "%j. ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
 by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
 qed "ack_le_mono2";
 
 (*PROPERTY A 6*)
-Goal "[| i:nat;  j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
+Goal "[| i \\<in> nat;  j \\<in> nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
 by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
 by (rtac ack_le_mono2 1);
@@ -98,14 +98,14 @@
 qed "ack2_le_ack1";
 
 (*PROPERTY A 7-, the single-step lemma*)
-Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(succ(i),j)";
+Goal "[| i \\<in> nat; j \\<in> nat |] ==> ack(i,j) < ack(succ(i),j)";
 by (rtac (ack_lt_mono2 RS lt_trans2) 1);
 by (rtac ack2_le_ack1 4);
 by Auto_tac;
 qed "ack_lt_ack_succ1";
 
 (*PROPERTY A 7, monotonicity for < *)
-Goal "[| i<j; j:nat; k:nat |] ==> ack(i,k) < ack(j,k)";
+Goal "[| i<j; j \\<in> nat; k \\<in> nat |] ==> ack(i,k) < ack(j,k)";
 by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
 by (etac succ_lt_induct 1);
 by (assume_tac 1);
@@ -114,25 +114,25 @@
 qed "ack_lt_mono1";
 
 (*PROPERTY A 7', monotonicity for le *)
-Goal "[| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
+Goal "[| i le j; j \\<in> nat; k \\<in> nat |] ==> ack(i,k) le ack(j,k)";
 by (res_inst_tac [("f", "%j. ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
 by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
 qed "ack_le_mono1";
 
 (*PROPERTY A 8*)
-Goal "j:nat ==> ack(1,j) = succ(succ(j))";
+Goal "j \\<in> nat ==> ack(1,j) = succ(succ(j))";
 by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "ack_1";
 
 (*PROPERTY A 9*)
-Goal "j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
+Goal "j \\<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
 by (induct_tac "j" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [ack_1, add_succ_right])));
 qed "ack_2";
 
 (*PROPERTY A 10*)
-Goal "[| i1:nat; i2:nat; j:nat |] ==> \
+Goal "[| i1 \\<in> nat; i2 \\<in> nat; j \\<in> nat |] ==> \
 \               ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)";
 by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
 by (Asm_simp_tac 1);
@@ -142,7 +142,7 @@
 qed "ack_nest_bound";
 
 (*PROPERTY A 11*)
-Goal "[| i1:nat; i2:nat; j:nat |] ==> \
+Goal "[| i1 \\<in> nat; i2 \\<in> nat; j \\<in> nat |] ==> \
 \          ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)";
 by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1);
 by (asm_simp_tac (simpset() addsimps [ack_2]) 1);
@@ -154,8 +154,8 @@
 qed "ack_add_bound";
 
 (*PROPERTY A 12.  Article uses existential quantifier but the ALF proof
-  used k#+4.  Quantified version must be nested EX k'. ALL i,j... *)
-Goal "[| i < ack(k,j);  j:nat;  k:nat |] ==> \
+  used k#+4.  Quantified version must be nested \\<exists>k'. \\<forall>i,j... *)
+Goal "[| i < ack(k,j);  j \\<in> nat;  k \\<in> nat |] ==> \
 \             i#+j < ack(succ(succ(succ(succ(k)))), j)";
 by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
 by (rtac (ack_add_bound RS lt_trans2) 2);
@@ -167,14 +167,14 @@
 
 Addsimps [list_add_type];
 
-Goalw [SC_def] "l: list(nat) ==> SC ` l < ack(1, list_add(l))";
+Goalw [SC_def] "l \\<in> list(nat) ==> SC ` l < ack(1, list_add(l))";
 by (exhaust_tac "l" 1);
 by (asm_simp_tac (simpset() addsimps [succ_iff]) 1);
 by (asm_simp_tac (simpset() addsimps [ack_1, add_le_self]) 1);
 qed "SC_case";
 
 (*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
-Goal "[| i:nat; j:nat |] ==> i < ack(i,j)";
+Goal "[| i \\<in> nat; j \\<in> nat |] ==> i < ack(i,j)";
 by (induct_tac "i" 1);
 by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
 by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
@@ -182,12 +182,12 @@
 qed "lt_ack1";
 
 Goalw [CONST_def]
-    "[| l: list(nat);  k: nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
+    "[| l \\<in> list(nat);  k \\<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
 by (asm_simp_tac (simpset() addsimps [lt_ack1]) 1);
 qed "CONST_case";
 
 Goalw [PROJ_def]
-    "l: list(nat) ==> ALL i:nat. PROJ(i) ` l < ack(0, list_add(l))";
+    "l \\<in> list(nat) ==> \\<forall>i \\<in> nat. PROJ(i) ` l < ack(0, list_add(l))";
 by (Asm_simp_tac 1);
 by (etac list.induct 1);
 by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1);
@@ -203,10 +203,10 @@
 
 (** COMP case **)
 
-Goal "fs : list({f: prim_rec .                                 \
-\                  EX kf:nat. ALL l:list(nat).                  \
+Goal "fs \\<in> list({f \\<in> prim_rec .                                 \
+\                  \\<exists>kf \\<in> nat. \\<forall>l \\<in> list(nat).                  \
 \                             f`l < ack(kf, list_add(l))})      \
-\      ==> EX k:nat. ALL l: list(nat).                          \
+\      ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat).                          \
 \                list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
 by (etac list.induct 1);
 by (res_inst_tac [("x","0")] bexI 1);
@@ -221,11 +221,11 @@
 
 Goalw [COMP_def]
  "[| kg: nat;                                 \
-\         ALL l:list(nat). g`l < ack(kg, list_add(l));          \
-\         fs : list({f: prim_rec .                               \
-\                    EX kf:nat. ALL l:list(nat).                \
+\         \\<forall>l \\<in> list(nat). g`l < ack(kg, list_add(l));          \
+\         fs \\<in> list({f \\<in> prim_rec .                               \
+\                    \\<exists>kf \\<in> nat. \\<forall>l \\<in> list(nat).                \
 \                       f`l < ack(kf, list_add(l))})            \
-\      |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
+\      |] ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
 by (Asm_simp_tac 1);
 by (ftac list_CollectD 1);
 by (etac (COMP_map_lemma RS bexE) 1);
@@ -240,11 +240,11 @@
 (** PREC case **)
 
 Goalw [PREC_def]
- "[| ALL l:list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \
-\           ALL l:list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \
-\           f: prim_rec;  kf: nat;                                       \
-\           g: prim_rec;  kg: nat;                                       \
-\           l: list(nat)                                                \
+ "[| \\<forall>l \\<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \
+\           \\<forall>l \\<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \
+\           f \\<in> prim_rec;  kf: nat;                                       \
+\           g \\<in> prim_rec;  kg: nat;                                       \
+\           l \\<in> list(nat)                                                \
 \        |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))";
 by (exhaust_tac "l" 1);
 by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
@@ -269,25 +269,25 @@
 by Auto_tac;
 qed "PREC_case_lemma";
 
-Goal "[| f: prim_rec;  kf: nat;                               \
-\        g: prim_rec;  kg: nat;                               \
-\        ALL l:list(nat). f`l < ack(kf, list_add(l));        \
-\        ALL l:list(nat). g`l < ack(kg, list_add(l))         \
-\     |] ==> EX k:nat. ALL l: list(nat). PREC(f,g)`l< ack(k, list_add(l))";
+Goal "[| f \\<in> prim_rec;  kf: nat;                               \
+\        g \\<in> prim_rec;  kg: nat;                               \
+\        \\<forall>l \\<in> list(nat). f`l < ack(kf, list_add(l));        \
+\        \\<forall>l \\<in> list(nat). g`l < ack(kg, list_add(l))         \
+\     |] ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). PREC(f,g)`l< ack(k, list_add(l))";
 by (rtac (ballI RS bexI) 1);
 by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
 by (REPEAT_FIRST (rtac (ack_add_bound2 RS ballI) THEN' etac bspec));
 by Typecheck_tac;
 qed "PREC_case";
 
-Goal "f:prim_rec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
+Goal "f \\<in> prim_rec ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> list(nat). f`l < ack(k, list_add(l))";
 by (etac prim_rec.induct 1);
 by (auto_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, 
 			      PREC_case], 
 	      simpset()));
 qed "ack_bounds_prim_rec";
 
-Goal "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : prim_rec";
+Goal "~ (\\<lambda>l \\<in> list(nat). list_case(0, %x xs. ack(x,x), l)) \\<in> prim_rec";
 by (rtac notI 1);
 by (etac (ack_bounds_prim_rec RS bexE) 1);
 by (rtac lt_irrefl 1);

--- a/src/ZF/ex/Primrec.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Primrec.thy	Mon May 21 14:36:24 2001 +0200
@@ -21,11 +21,11 @@
 inductive
   domains "prim_rec" <= "list(nat)->nat"
   intrs
-    SC       "SC : prim_rec"
-    CONST    "k: nat ==> CONST(k) : prim_rec"
-    PROJ     "i: nat ==> PROJ(i) : prim_rec"
-    COMP     "[| g: prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec"
-    PREC     "[| f: prim_rec; g: prim_rec |] ==> PREC(f,g): prim_rec"
+    SC       "SC \\<in> prim_rec"
+    CONST    "k \\<in> nat ==> CONST(k) \\<in> prim_rec"
+    PROJ     "i \\<in> nat ==> PROJ(i) \\<in> prim_rec"
+    COMP     "[| g \\<in> prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec"
+    PREC     "[| f \\<in> prim_rec; g \\<in> prim_rec |] ==> PREC(f,g): prim_rec"
   monos       list_mono
   con_defs    SC_def, CONST_def, PROJ_def, COMP_def, PREC_def
   type_intrs "nat_typechecks @ list.intrs @

--- a/src/ZF/ex/Primrec_defs.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Primrec_defs.ML	Mon May 21 14:36:24 2001 +0200
@@ -11,28 +11,28 @@
 
 (** Useful special cases of evaluation ***)
 
-Goalw [SC_def] "[| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
+Goalw [SC_def] "[| x \\<in> nat;  l \\<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
 by (Asm_simp_tac 1);
 qed "SC";
 
-Goalw [CONST_def] "[| l: list(nat) |] ==> CONST(k) ` l = k";
+Goalw [CONST_def] "[| l \\<in> list(nat) |] ==> CONST(k) ` l = k";
 by (Asm_simp_tac 1);
 qed "CONST";
 
-Goalw [PROJ_def] "[| x: nat;  l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
+Goalw [PROJ_def] "[| x \\<in> nat;  l \\<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
 by (Asm_simp_tac 1);
 qed "PROJ_0";
 
-Goalw [COMP_def] "[| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
+Goalw [COMP_def] "[| l \\<in> list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
 by (Asm_simp_tac 1);
 qed "COMP_1";
 
-Goalw [PREC_def] "l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
+Goalw [PREC_def] "l \\<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
 by (Asm_simp_tac 1);
 qed "PREC_0";
 
 Goalw [PREC_def]
-    "[| x:nat;  l: list(nat) |] ==>  \
+    "[| x \\<in> nat;  l \\<in> list(nat) |] ==>  \
 \         PREC(f,g) ` (Cons(succ(x),l)) = \
 \         g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
 by (Asm_simp_tac 1);

--- a/src/ZF/ex/Primrec_defs.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Primrec_defs.thy	Mon May 21 14:36:24 2001 +0200
@@ -25,17 +25,17 @@
 
 defs
 
-  SC_def    "SC == lam l:list(nat).list_case(0, %x xs. succ(x), l)"
+  SC_def    "SC == \\<lambda>l \\<in> list(nat).list_case(0, %x xs. succ(x), l)"
 
-  CONST_def "CONST(k) == lam l:list(nat).k"
+  CONST_def "CONST(k) == \\<lambda>l \\<in> list(nat).k"
 
-  PROJ_def  "PROJ(i) == lam l:list(nat). list_case(0, %x xs. x, drop(i,l))"
+  PROJ_def  "PROJ(i) == \\<lambda>l \\<in> list(nat). list_case(0, %x xs. x, drop(i,l))"
 
-  COMP_def  "COMP(g,fs) == lam l:list(nat). g ` List.map(%f. f`l, fs)"
+  COMP_def  "COMP(g,fs) == \\<lambda>l \\<in> list(nat). g ` List.map(%f. f`l, fs)"
 
   (*Note that g is applied first to PREC(f,g)`y and then to y!*)
   PREC_def  "PREC(f,g) == 
-            lam l:list(nat). list_case(0, 
+            \\<lambda>l \\<in> list(nat). list_case(0, 
                       %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
   
 primrec

--- a/src/ZF/ex/PropLog.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/PropLog.ML	Mon May 21 14:36:24 2001 +0200
@@ -6,7 +6,7 @@
 Inductive definition of propositional logic.
 Soundness and completeness w.r.t. truth-tables.
 
-Prove: If H|=p then G|=p where G:Fin(H)
+Prove: If H|=p then G|=p where G \\<in> Fin(H)
 *)
 
 Addsimps prop.intrs;
@@ -19,7 +19,7 @@
 by (Simp_tac 1);
 qed "is_true_Fls";
 
-Goalw [is_true_def] "is_true(#v,t) <-> v:t";
+Goalw [is_true_def] "is_true(#v,t) <-> v \\<in> t";
 by (Simp_tac 1);
 qed "is_true_Var";
 
@@ -32,7 +32,7 @@
 
 (*** Proof theory of propositional logic ***)
 
-Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
+Goalw thms.defs "G \\<subseteq> H ==> thms(G) \\<subseteq> thms(H)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac thms.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
@@ -40,7 +40,7 @@
 
 val thms_in_pl = thms.dom_subset RS subsetD;
 
-val ImpE = prop.mk_cases "p=>q : prop";
+val ImpE = prop.mk_cases "p=>q \\<in> prop";
 
 (*Stronger Modus Ponens rule: no typechecking!*)
 Goal "[| H |- p=>q;  H |- p |] ==> H |- q";
@@ -49,7 +49,7 @@
 qed "thms_MP";
 
 (*Rule is called I for Identity Combinator, not for Introduction*)
-Goal "p:prop ==> H |- p=>p";
+Goal "p \\<in> prop ==> H |- p=>p";
 by (rtac (thms.S RS thms_MP RS thms_MP) 1);
 by (rtac thms.K 5);
 by (rtac thms.K 4);
@@ -58,7 +58,7 @@
 
 (** Weakening, left and right **)
 
-(* [| G<=H;  G|-p |] ==> H|-p   Order of premises is convenient with RS*)
+(* [| G \\<subseteq> H;  G|-p |] ==> H|-p   Order of premises is convenient with RS*)
 bind_thm ("weaken_left", (thms_mono RS subsetD));
 
 (* H |- p ==> cons(a,H) |- p *)
@@ -67,13 +67,13 @@
 val weaken_left_Un1  = Un_upper1 RS weaken_left;
 val weaken_left_Un2  = Un_upper2 RS weaken_left;
 
-Goal "[| H |- q;  p:prop |] ==> H |- p=>q";
+Goal "[| H |- q;  p \\<in> prop |] ==> H |- p=>q";
 by (rtac (thms.K RS thms_MP) 1);
 by (REPEAT (ares_tac [thms_in_pl] 1));
 qed "weaken_right";
 
 (*The deduction theorem*)
-Goal "[| cons(p,H) |- q;  p:prop |] ==>  H |- p=>q";
+Goal "[| cons(p,H) |- q;  p \\<in> prop |] ==>  H |- p=>q";
 by (etac thms.induct 1);
 by (blast_tac (claset() addIs [thms_I, thms.H RS weaken_right]) 1);
 by (blast_tac (claset() addIs [thms.K RS weaken_right]) 1);
@@ -89,13 +89,13 @@
 by (REPEAT (ares_tac [thms_in_pl] 1));
 qed "cut";
 
-Goal "[| H |- Fls; p:prop |] ==> H |- p";
+Goal "[| H |- Fls; p \\<in> prop |] ==> H |- p";
 by (rtac (thms.DN RS thms_MP) 1);
 by (rtac weaken_right 2);
 by (REPEAT (ares_tac (prop.intrs@[consI1]) 1));
 qed "thms_FlsE";
 
-(* [| H |- p=>Fls;  H |- p;  q: prop |] ==> H |- q *)
+(* [| H |- p=>Fls;  H |- p;  q \\<in> prop |] ==> H |- q *)
 bind_thm ("thms_notE", (thms_MP RS thms_FlsE));
 
 (*Soundness of the rules wrt truth-table semantics*)
@@ -107,7 +107,7 @@
 (*** Towards the completeness proof ***)
 
 val [premf,premq] = goal PropLog.thy
-    "[| H |- p=>Fls; q: prop |] ==> H |- p=>q";
+    "[| H |- p=>Fls; q \\<in> prop |] ==> H |- p=>q";
 by (rtac (premf RS thms_in_pl RS ImpE) 1);
 by (rtac deduction 1);
 by (rtac (premf RS weaken_left_cons RS thms_notE) 1);
@@ -126,7 +126,7 @@
 qed "Imp_Fls";
 
 (*Typical example of strengthening the induction formula*)
-Goal "p: prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)";
+Goal "p \\<in> prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)";
 by (Simp_tac 1);
 by (induct_tac "p" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H])));
@@ -137,7 +137,7 @@
 qed "hyps_thms_if";
 
 (*Key lemma for completeness; yields a set of assumptions satisfying p*)
-Goalw [logcon_def] "[| p: prop;  0 |= p |] ==> hyps(p,t) |- p";
+Goalw [logcon_def] "[| p \\<in> prop;  0 |= p |] ==> hyps(p,t) |- p";
 by (dtac hyps_thms_if 1);
 by (Asm_full_simp_tac 1);
 qed "logcon_thms_p";
@@ -148,14 +148,14 @@
           addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
 
 (*The excluded middle in the form of an elimination rule*)
-Goal "[| p: prop;  q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
+Goal "[| p \\<in> prop;  q \\<in> prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
 by (rtac (deduction RS deduction) 1);
 by (rtac (thms.DN RS thms_MP) 1);
 by (ALLGOALS (blast_tac thms_cs));
 qed "thms_excluded_middle";
 
 (*Hard to prove directly because it requires cuts*)
-Goal "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p: prop |] ==> H |- q";
+Goal "[| cons(p,H) |- q;  cons(p=>Fls,H) |- q;  p \\<in> prop |] ==> H |- q";
 by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
 by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1));
 qed "thms_excluded_middle_rule";
@@ -163,32 +163,32 @@
 (*** Completeness -- lemmas for reducing the set of assumptions ***)
 
 (*For the case hyps(p,t)-cons(#v,Y) |- p;
-  we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-Goal "p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
+  we also have hyps(p,t)-{#v} \\<subseteq> hyps(p, t-{v}) *)
+Goal "p \\<in> prop ==> hyps(p, t-{v}) \\<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})";
 by (induct_tac "p" 1);
 by Auto_tac;
 qed "hyps_Diff";
 
 (*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
-  we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
-Goal "p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
+  we also have hyps(p,t)-{#v=>Fls} \\<subseteq> hyps(p, cons(v,t)) *)
+Goal "p \\<in> prop ==> hyps(p, cons(v,t)) \\<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})";
 by (induct_tac "p" 1);
 by Auto_tac;
 qed "hyps_cons";
 
 (** Two lemmas for use with weaken_left **)
 
-Goal "B-C <= cons(a, B-cons(a,C))";
+Goal "B-C \\<subseteq> cons(a, B-cons(a,C))";
 by (Fast_tac 1);
 qed "cons_Diff_same";
 
-Goal "cons(a, B-{c}) - D <= cons(a, B-cons(c,D))";
+Goal "cons(a, B-{c}) - D \\<subseteq> cons(a, B-cons(c,D))";
 by (Fast_tac 1);
 qed "cons_Diff_subset2";
 
 (*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
- could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
-Goal "p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
+ could probably prove the stronger hyps(p,t) \\<in> Fin(hyps(p,0) Un hyps(p,nat))*)
+Goal "p \\<in> prop ==> hyps(p,t) \\<in> Fin(\\<Union>v \\<in> nat. {#v, #v=>Fls})";
 by (induct_tac "p" 1);
 by Auto_tac;  
 qed "hyps_finite";
@@ -198,7 +198,7 @@
 (*Induction on the finite set of assumptions hyps(p,t0).
   We may repeatedly subtract assumptions until none are left!*)
 val [premp,sat] = goal PropLog.thy
-    "[| p: prop;  0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
+    "[| p \\<in> prop;  0 |= p |] ==> \\<forall>t. hyps(p,t) - hyps(p,t0) |- p";
 by (rtac (premp RS hyps_finite RS Fin_induct) 1);
 by (simp_tac (simpset() addsimps [premp, sat, logcon_thms_p, Diff_0]) 1);
 by Safe_tac;
@@ -221,7 +221,7 @@
 qed "completeness_0_lemma";
 
 (*The base case for completeness*)
-val [premp,sat] = goal PropLog.thy "[| p: prop;  0 |= p |] ==> 0 |- p";
+val [premp,sat] = goal PropLog.thy "[| p \\<in> prop;  0 |= p |] ==> 0 |- p";
 by (rtac (Diff_cancel RS subst) 1);
 by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1);
 qed "completeness_0";
@@ -231,7 +231,7 @@
 by Auto_tac;
 qed "logcon_Imp";
 
-Goal "H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p";
+Goal "H \\<in> Fin(prop) ==> \\<forall>p \\<in> prop. H |= p --> H |- p";
 by (etac Fin_induct 1);
 by (safe_tac (claset() addSIs [completeness_0]));
 by (rtac (weaken_left_cons RS thms_MP) 1);
@@ -241,7 +241,7 @@
 
 val completeness = completeness_lemma RS bspec RS mp;
 
-val [finite] = goal PropLog.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop";
+val [finite] = goal PropLog.thy "H \\<in> Fin(prop) ==> H |- p <-> H |= p & p \\<in> prop";
 by (fast_tac (claset() addSEs [soundness, finite RS completeness, 
 			       thms_in_pl]) 1);
 qed "thms_iff";

--- a/src/ZF/ex/PropLog.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/PropLog.thy	Mon May 21 14:36:24 2001 +0200
@@ -15,8 +15,8 @@
 
 datatype
   "prop" = Fls
-         | Var ("n: nat")                       ("#_" [100] 100)
-         | "=>" ("p: prop", "q: prop")          (infixr 90)
+         | Var ("n \\<in> nat")                       ("#_" [100] 100)
+         | "=>" ("p \\<in> prop", "q \\<in> prop")          (infixr 90)
 
 (** The proof system **)
 consts
@@ -26,16 +26,16 @@
   "|-"     :: [i,i] => o                        (infixl 50)
 
 translations
-  "H |- p" == "p : thms(H)"
+  "H |- p" == "p \\<in> thms(H)"
 
 inductive
   domains "thms(H)" <= "prop"
   intrs
-    H  "[| p:H;  p:prop |] ==> H |- p"
-    K  "[| p:prop;  q:prop |] ==> H |- p=>q=>p"
-    S  "[| p:prop;  q:prop;  r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
-    DN "p:prop ==> H |- ((p=>Fls) => Fls) => p"
-    MP "[| H |- p=>q;  H |- p;  p:prop;  q:prop |] ==> H |- q"
+    H  "[| p \\<in> H;  p \\<in> prop |] ==> H |- p"
+    K  "[| p \\<in> prop;  q \\<in> prop |] ==> H |- p=>q=>p"
+    S  "[| p \\<in> prop;  q \\<in> prop;  r \\<in> prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
+    DN "p \\<in> prop ==> H |- ((p=>Fls) => Fls) => p"
+    MP "[| H |- p=>q;  H |- p;  p \\<in> prop;  q \\<in> prop |] ==> H |- q"
   type_intrs "prop.intrs"
 
 
@@ -52,16 +52,16 @@
 defs
   (*Logical consequence: for every valuation, if all elements of H are true
      then so is p*)
-  logcon_def  "H |= p == ALL t. (ALL q:H. is_true(q,t)) --> is_true(p,t)"
+  logcon_def  "H |= p == \\<forall>t. (\\<forall>q \\<in> H. is_true(q,t)) --> is_true(p,t)"
 
 primrec (** A finite set of hypotheses from t and the Vars in p **)
   "hyps(Fls, t)    = 0"
-  "hyps(Var(v), t) = (if v:t then {#v} else {#v=>Fls})"
+  "hyps(Var(v), t) = (if v \\<in> t then {#v} else {#v=>Fls})"
   "hyps(p=>q, t)   = hyps(p,t) Un hyps(q,t)"
  
 primrec (** Semantics of propositional logic **)
   "is_true_fun(Fls, t)    = 0"
-  "is_true_fun(Var(v), t) = (if v:t then 1 else 0)"
+  "is_true_fun(Var(v), t) = (if v \\<in> t then 1 else 0)"
   "is_true_fun(p=>q, t)   = (if is_true_fun(p,t)=1 then is_true_fun(q,t)
 			     else 1)"

--- a/src/ZF/ex/Ramsey.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Ramsey.ML	Mon May 21 14:36:24 2001 +0200
@@ -43,17 +43,17 @@
 qed "Atleast0";
 
 Goalw [Atleast_def]
-    "Atleast(succ(m),A) ==> EX x:A. Atleast(m, A-{x})";
+    "Atleast(succ(m),A) ==> \\<exists>x \\<in> A. Atleast(m, A-{x})";
 by (fast_tac (claset() addEs [inj_is_fun RS apply_type, inj_succ_restrict]) 1);
 qed "Atleast_succD";
 
 Goalw [Atleast_def]
-    "[| Atleast(n,A);  A<=B |] ==> Atleast(n,B)";
+    "[| Atleast(n,A);  A \\<subseteq> B |] ==> Atleast(n,B)";
 by (fast_tac (claset() addEs [inj_weaken_type]) 1);
 qed "Atleast_superset";
 
 Goalw [Atleast_def,succ_def]
-    "[| Atleast(m,B);  b~: B |] ==> Atleast(succ(m), cons(b,B))";
+    "[| Atleast(m,B);  b\\<notin> B |] ==> Atleast(succ(m), cons(b,B))";
 by (etac exE 1);
 by (rtac exI 1);
 by (etac inj_extend 1);
@@ -61,7 +61,7 @@
 by (assume_tac 1);
 qed "Atleast_succI";
 
-Goal "[| Atleast(m, B-{x});  x: B |] ==> Atleast(succ(m), B)";
+Goal "[| Atleast(m, B-{x});  x \\<in> B |] ==> Atleast(succ(m), B)";
 by (etac (Atleast_succI RS Atleast_superset) 1);
 by (Fast_tac 1);
 by (Fast_tac 1);
@@ -71,8 +71,8 @@
 
 (*The #-succ(0) strengthens the original theorem statement, but precisely
   the same proof could be used!!*)
-Goal "m: nat ==> \
-\     ALL n: nat. ALL A B. Atleast((m#+n) #- succ(0), A Un B) -->   \
+Goal "m \\<in> nat ==> \
+\     \\<forall>n \\<in> nat. \\<forall>A B. Atleast((m#+n) #- succ(0), A Un B) -->   \
 \                          Atleast(m,A) | Atleast(n,B)";
 by (induct_tac "m" 1);
 by (fast_tac (claset() addSIs [Atleast0]) 1);
@@ -86,14 +86,14 @@
 by (etac (Atleast_succD RS bexE) 1);
 by (rename_tac "n' A B z" 1);
 by (etac UnE 1);
-(**case z:B.  Instantiate the 'ALL A B' induction hypothesis. **)
+(**case z \\<in> B.  Instantiate the '\\<forall>A B' induction hypothesis. **)
 by (dres_inst_tac [("x1","A"), ("x","B-{z}")] (spec RS spec) 2);
 by (etac (mp RS disjE) 2);
 (*cases Atleast(succ(m1),A) and Atleast(succ(k),B)*)
 by (REPEAT (eresolve_tac [asm_rl, notE, Atleast_Diff_succI] 3));
 (*proving the condition*)
 by (etac Atleast_superset 2 THEN Fast_tac 2);
-(**case z:A.  Instantiate the 'ALL n:nat. ALL A B' induction hypothesis. **)
+(**case z \\<in> A.  Instantiate the '\\<forall>n \\<in> nat. \\<forall>A B' induction hypothesis. **)
 by (dres_inst_tac [("x2","succ(n')"), ("x1","A-{z}"), ("x","B")] 
     (bspec RS spec RS spec) 1);
 by (etac nat_succI 1);
@@ -122,24 +122,24 @@
 
 (*The use of succ(m) here, rather than #-succ(0), simplifies the proof of 
   Ramsey_step_lemma.*)
-Goal "[| Atleast(m #+ n, A);  m: nat;  n: nat |]  \
-\     ==> Atleast(succ(m), {x:A. ~P(x)}) | Atleast(n, {x:A. P(x)})";
+Goal "[| Atleast(m #+ n, A);  m \\<in> nat;  n \\<in> nat |]  \
+\     ==> Atleast(succ(m), {x \\<in> A. ~P(x)}) | Atleast(n, {x \\<in> A. P(x)})";
 by (rtac (nat_succI RS pigeon2) 1);
 by (Asm_simp_tac 3);
 by (rtac Atleast_superset 3);
 by Auto_tac;
 qed "Atleast_partition";
 
-(*For the Atleast part, proves ~(a:I) from the second premise!*)
+(*For the Atleast part, proves ~(a \\<in> I) from the second premise!*)
 Goalw [Symmetric_def,Indept_def]
-    "[| Symmetric(E);  Indept(I, {z: V-{a}. <a,z> ~: E}, E);  a: V;  \
+    "[| Symmetric(E);  Indept(I, {z \\<in> V-{a}. <a,z> \\<notin> E}, E);  a \\<in> V;  \
 \       Atleast(j,I) |] ==>   \
 \    Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
 by (blast_tac (claset() addSIs [Atleast_succI]) 1);
 qed "Indept_succ";
 
 Goalw [Symmetric_def,Clique_def]
-    "[| Symmetric(E);  Clique(C, {z: V-{a}. <a,z>:E}, E);  a: V;  \
+    "[| Symmetric(E);  Clique(C, {z \\<in> V-{a}. <a,z>:E}, E);  a \\<in> V;  \
 \       Atleast(j,C) |] ==>   \
 \    Clique(cons(a,C), V, E) & Atleast(succ(j), cons(a,C))";
 by (blast_tac (claset() addSIs [Atleast_succI]) 1);
@@ -150,7 +150,7 @@
 (*Published proofs gloss over the need for Ramsey numbers to be POSITIVE.*)
 val ram1::ram2::prems = goalw Ramsey.thy [Ramsey_def] 
    "[| Ramsey(succ(m), succ(i), j);  Ramsey(n, i, succ(j));  \
-\      m: nat;  n: nat |] ==> \
+\      m \\<in> nat;  n \\<in> nat |] ==> \
 \   Ramsey(succ(m#+n), succ(i), succ(j))";
 by Safe_tac;
 by (etac (Atleast_succD RS bexE) 1);
@@ -161,7 +161,7 @@
 by (Fast_tac 1);
 by (fast_tac (claset() addEs [Clique_superset]) 1); (*easy -- given a Clique*)
 by Safe_tac;
-by (eresolve_tac (swapify [exI]) 1);             (*ignore main EX quantifier*)
+by (eresolve_tac (swapify [exI]) 1);             (*ignore main \\<exists>quantifier*)
 by (REPEAT (ares_tac [Indept_succ] 1));          (*make a bigger Indept*)
 (*case n*)
 by (rtac (ram2 RS spec RS spec RS mp RS disjE) 1);
@@ -176,7 +176,7 @@
 (** The actual proof **)
 
 (*Again, the induction requires Ramsey numbers to be positive.*)
-Goal "i: nat ==> ALL j: nat. EX n:nat. Ramsey(succ(n), i, j)";
+Goal "i \\<in> nat ==> \\<forall>j \\<in> nat. \\<exists>n \\<in> nat. Ramsey(succ(n), i, j)";
 by (induct_tac "i" 1);
 by (fast_tac (claset() addSIs [Ramsey0j]) 1);
 by (rtac ballI 1);
@@ -187,7 +187,7 @@
 qed "ramsey_lemma";
 
 (*Final statement in a tidy form, without succ(...) *)
-Goal "[| i: nat;  j: nat |] ==> EX n:nat. Ramsey(n,i,j)";
+Goal "[| i \\<in> nat;  j \\<in> nat |] ==> \\<exists>n \\<in> nat. Ramsey(n,i,j)";
 by (best_tac (claset() addDs [ramsey_lemma]) 1);
 qed "ramsey";

--- a/src/ZF/ex/Ramsey.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Ramsey.thy	Mon May 21 14:36:24 2001 +0200
@@ -27,20 +27,20 @@
 defs
 
   Symmetric_def
-    "Symmetric(E) == (ALL x y. <x,y>:E --> <y,x>:E)"
+    "Symmetric(E) == (\\<forall>x y. <x,y>:E --> <y,x>:E)"
 
   Clique_def
-    "Clique(C,V,E) == (C<=V) & (ALL x:C. ALL y:C. x~=y --> <x,y> : E)"
+    "Clique(C,V,E) == (C \\<subseteq> V) & (\\<forall>x \\<in> C. \\<forall>y \\<in> C. x\\<noteq>y --> <x,y> \\<in> E)"
 
   Indept_def
-    "Indept(I,V,E) == (I<=V) & (ALL x:I. ALL y:I. x~=y --> <x,y> ~: E)"
+    "Indept(I,V,E) == (I \\<subseteq> V) & (\\<forall>x \\<in> I. \\<forall>y \\<in> I. x\\<noteq>y --> <x,y> \\<notin> E)"
 
   Atleast_def
-    "Atleast(n,S) == (EX f. f: inj(n,S))"
+    "Atleast(n,S) == (\\<exists>f. f \\<in> inj(n,S))"
 
   Ramsey_def
-    "Ramsey(n,i,j) == ALL V E. Symmetric(E) & Atleast(n,V) -->  
-         (EX C. Clique(C,V,E) & Atleast(i,C)) |       
-         (EX I. Indept(I,V,E) & Atleast(j,I))"
+    "Ramsey(n,i,j) == \\<forall>V E. Symmetric(E) & Atleast(n,V) -->  
+         (\\<exists>C. Clique(C,V,E) & Atleast(i,C)) |       
+         (\\<exists>I. Indept(I,V,E) & Atleast(j,I))"
 
 end

--- a/src/ZF/ex/Rmap.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Rmap.ML	Mon May 21 14:36:24 2001 +0200
@@ -6,26 +6,26 @@
 Inductive definition of an operator to "map" a relation over a list
 *)
 
-Goalw rmap.defs "r<=s ==> rmap(r) <= rmap(s)";
+Goalw rmap.defs "r \\<subseteq> s ==> rmap(r) \\<subseteq> rmap(s)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac rmap.bnd_mono 1));
 by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ 
                       basic_monos) 1));
 qed "rmap_mono";
 
-val Nil_rmap_case  = rmap.mk_cases "<Nil,zs> : rmap(r)"
-and Cons_rmap_case = rmap.mk_cases "<Cons(x,xs),zs> : rmap(r)";
+val Nil_rmap_case  = rmap.mk_cases "<Nil,zs> \\<in> rmap(r)"
+and Cons_rmap_case = rmap.mk_cases "<Cons(x,xs),zs> \\<in> rmap(r)";
 
 AddIs  rmap.intrs;
 AddSEs [Nil_rmap_case, Cons_rmap_case];
 
-Goal "r <= A*B ==> rmap(r) <= list(A)*list(B)";
+Goal "r \\<subseteq> A*B ==> rmap(r) \\<subseteq> list(A)*list(B)";
 by (rtac (rmap.dom_subset RS subset_trans) 1);
 by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
                       Sigma_mono, list_mono] 1));
 qed "rmap_rel_type";
 
-Goal "A <= domain(r) ==> list(A) <= domain(rmap(r))";
+Goal "A \\<subseteq> domain(r) ==> list(A) \\<subseteq> domain(rmap(r))";
 by (rtac subsetI 1);
 by (etac list.induct 1);
 by (ALLGOALS Fast_tac);
@@ -40,7 +40,7 @@
 
 (** If f is a function then rmap(f) behaves as expected. **)
 
-Goal "f: A->B ==> rmap(f): list(A)->list(B)";
+Goal "f \\<in> A->B ==> rmap(f): list(A)->list(B)";
 by (asm_full_simp_tac (simpset() addsimps [Pi_iff, rmap_rel_type,
 					   rmap_functional, rmap_total]) 1);
 qed "rmap_fun_type";
@@ -49,7 +49,7 @@
 by (Blast_tac 1);
 qed "rmap_Nil";
 
-Goal "[| f: A->B;  x: A;  xs: list(A) |]  \
+Goal "[| f \\<in> A->B;  x \\<in> A;  xs: list(A) |]  \
 \     ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
 by (rtac apply_equality 1);
 by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));

--- a/src/ZF/ex/Rmap.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Rmap.thy	Mon May 21 14:36:24 2001 +0200
@@ -14,10 +14,10 @@
 inductive
   domains "rmap(r)" <= "list(domain(r))*list(range(r))"
   intrs
-    NilI  "<Nil,Nil> : rmap(r)"
+    NilI  "<Nil,Nil> \\<in> rmap(r)"
 
-    ConsI "[| <x,y>: r;  <xs,ys> : rmap(r) |] ==> 
-          <Cons(x,xs), Cons(y,ys)> : rmap(r)"
+    ConsI "[| <x,y>: r;  <xs,ys> \\<in> rmap(r) |] ==> 
+          <Cons(x,xs), Cons(y,ys)> \\<in> rmap(r)"
 
   type_intrs "[domainI,rangeI] @ list.intrs"

--- a/src/ZF/ex/TF.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/TF.ML	Mon May 21 14:36:24 2001 +0200
@@ -13,11 +13,11 @@
 
 val [_, tree_def, forest_def] = tree_forest.defs;
 
-Goalw [tree_def] "tree(A) <= tree_forest(A)";
+Goalw [tree_def] "tree(A) \\<subseteq> tree_forest(A)";
 by (rtac Part_subset 1);
 qed "tree_subset_TF";
 
-Goalw [forest_def] "forest(A) <= tree_forest(A)";
+Goalw [forest_def] "forest(A) \\<subseteq> tree_forest(A)";
 by (rtac Part_subset 1);
 qed "forest_subset_TF";
 
@@ -40,13 +40,13 @@
                           tree_forest_unfold;
 
 Goalw [tree_def, forest_def]
-    "tree(A) = {Inl(x). x: A*forest(A)}";
+    "tree(A) = {Inl(x). x \\<in> A*forest(A)}";
 by (rtac (Part_Inl RS subst) 1);
 by (rtac (tree_forest_unfold' RS subst_context) 1);
 qed "tree_unfold";
 
 Goalw [tree_def, forest_def]
-    "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
+    "forest(A) = {Inr(x). x \\<in> {0} + tree(A)*forest(A)}";
 by (rtac (Part_Inr RS subst) 1);
 by (rtac (tree_forest_unfold' RS subst_context) 1);
 qed "forest_unfold";
@@ -55,26 +55,26 @@
 (** Type checking for recursor: Not needed; possibly interesting (??) **)
 
 val major::prems = goal TF.thy
-    "[| z: tree_forest(A);  \
-\       !!x f r. [| x: A;  f: forest(A);  r: C(f)               \
+    "[| z \\<in> tree_forest(A);  \
+\       !!x f r. [| x \\<in> A;  f \\<in> forest(A);  r \\<in> C(f)               \
 \                 |] ==> b(x,f,r): C(Tcons(x,f));       \
-\       c : C(Fnil);                                            \
-\       !!t f r1 r2. [| t: tree(A);  f: forest(A);  r1: C(t); r2: C(f) \
+\       c \\<in> C(Fnil);                                            \
+\       !!t f r1 r2. [| t \\<in> tree(A);  f \\<in> forest(A);  r1: C(t); r2: C(f) \
 \                     |] ==> d(t,f,r1,r2): C(Fcons(t,f))        \
-\    |] ==> tree_forest_rec(b,c,d,z) : C(z)";
+\    |] ==> tree_forest_rec(b,c,d,z) \\<in> C(z)";
 by (rtac (major RS tree_forest.induct) 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
 qed "TF_rec_type";
 
 (*Mutually recursive version*)
 val prems = goal TF.thy
-    "[| !!x f r. [| x: A;  f: forest(A);  r: D(f)               \
+    "[| !!x f r. [| x \\<in> A;  f \\<in> forest(A);  r \\<in> D(f)               \
 \                 |] ==> b(x,f,r): C(Tcons(x,f));               \
-\       c : D(Fnil);                                            \
-\       !!t f r1 r2. [| t: tree(A);  f: forest(A);  r1: C(t); r2: D(f) \
+\       c \\<in> D(Fnil);                                            \
+\       !!t f r1 r2. [| t \\<in> tree(A);  f \\<in> forest(A);  r1: C(t); r2: D(f) \
 \                     |] ==> d(t,f,r1,r2): D(Fcons(t,f))        \
-\    |] ==> (ALL t:tree(A).    tree_forest_rec(b,c,d,t)  : C(t)) &       \
-\           (ALL f: forest(A). tree_forest_rec(b,c,d,f) : D(f))";
+\    |] ==> (\\<forall>t \\<in> tree(A).    tree_forest_rec(b,c,d,t)  \\<in> C(t)) &       \
+\           (\\<forall>f \\<in> forest(A). tree_forest_rec(b,c,d,f) \\<in> D(f))";
 by (rewtac Ball_def);
 by (rtac tree_forest.mutual_induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
@@ -83,12 +83,12 @@
 
 (** list_of_TF and of_list **)
 
-Goal "z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
+Goal "z \\<in> tree_forest(A) ==> list_of_TF(z) \\<in> list(tree(A))";
 by (etac tree_forest.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "list_of_TF_type";
 
-Goal "l: list(tree(A)) ==> of_list(l) : forest(A)";
+Goal "l \\<in> list(tree(A)) ==> of_list(l) \\<in> forest(A)";
 by (etac list.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "of_list_type";
@@ -97,9 +97,9 @@
 (** map **)
 
 val prems = Goal
-    "[| !!x. x: A ==> h(x): B |] ==> \
-\      (ALL t:tree(A). map(h,t) : tree(B)) &  \
-\      (ALL f: forest(A). map(h,f) : forest(B))";
+    "[| !!x. x \\<in> A ==> h(x): B |] ==> \
+\      (\\<forall>t \\<in> tree(A). map(h,t) \\<in> tree(B)) &  \
+\      (\\<forall>f \\<in> forest(A). map(h,f) \\<in> forest(B))";
 by (rewtac Ball_def);
 by (rtac tree_forest.mutual_induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
@@ -108,7 +108,7 @@
 
 (** size **)
 
-Goal "z: tree_forest(A) ==> size(z) : nat";
+Goal "z \\<in> tree_forest(A) ==> size(z) \\<in> nat";
 by (etac tree_forest.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "size_type";
@@ -116,7 +116,7 @@
 
 (** preorder **)
 
-Goal "z: tree_forest(A) ==> preorder(z) : list(A)";
+Goal "z \\<in> tree_forest(A) ==> preorder(z) \\<in> list(A)";
 by (etac tree_forest.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "preorder_type";
@@ -133,15 +133,15 @@
 
 (*essentially the same as list induction*)
 val major::prems = Goal
-    "[| f: forest(A);   \
+    "[| f \\<in> forest(A);   \
 \       R(Fnil);        \
-\       !!t f. [| t: tree(A);  f: forest(A);  R(f) |] ==> R(Fcons(t,f))  \
+\       !!t f. [| t \\<in> tree(A);  f \\<in> forest(A);  R(f) |] ==> R(Fcons(t,f))  \
 \    |] ==> R(f)";
 by (rtac (major RS (tree_forest.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
 by (REPEAT (ares_tac (TrueI::prems) 1));
 qed "forest_induct";
 
-Goal "f: forest(A) ==> of_list(list_of_TF(f)) = f";
+Goal "f \\<in> forest(A) ==> of_list(list_of_TF(f)) = f";
 by (etac forest_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "forest_iso";
@@ -153,31 +153,31 @@
 
 (** theorems about map **)
 
-Goal "z: tree_forest(A) ==> map(%u. u, z) = z";
+Goal "z \\<in> tree_forest(A) ==> map(%u. u, z) = z";
 by (etac tree_forest.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_ident";
 
-Goal "z: tree_forest(A) ==> map(h, map(j,z)) = map(%u. h(j(u)), z)";
+Goal "z \\<in> tree_forest(A) ==> map(h, map(j,z)) = map(%u. h(j(u)), z)";
 by (etac tree_forest.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "map_compose";
 
 (** theorems about size **)
 
-Goal "z: tree_forest(A) ==> size(map(h,z)) = size(z)";
+Goal "z \\<in> tree_forest(A) ==> size(map(h,z)) = size(z)";
 by (etac tree_forest.induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "size_map";
 
-Goal "z: tree_forest(A) ==> size(z) = length(preorder(z))";
+Goal "z \\<in> tree_forest(A) ==> size(z) = length(preorder(z))";
 by (etac tree_forest.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
 qed "size_length";
 
 (** theorems about preorder **)
 
-Goal "z: tree_forest(A) ==> preorder(TF.map(h,z)) = List.map(h, preorder(z))";
+Goal "z \\<in> tree_forest(A) ==> preorder(TF.map(h,z)) = List.map(h, preorder(z))";
 by (etac tree_forest.induct 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
 qed "preorder_map";

--- a/src/ZF/ex/TF.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/TF.thy	Mon May 21 14:36:24 2001 +0200
@@ -11,9 +11,9 @@
   tree, forest, tree_forest    :: i=>i
 
 datatype
-  "tree(A)"   = Tcons ("a: A",  "f: forest(A)")
+  "tree(A)"   = Tcons ("a \\<in> A",  "f \\<in> forest(A)")
 and
-  "forest(A)" = Fnil  |  Fcons ("t: tree(A)",  "f: forest(A)")
+  "forest(A)" = Fnil  |  Fcons ("t \\<in> tree(A)",  "f \\<in> forest(A)")
 
 
 consts

--- a/src/ZF/ex/Term.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Term.ML	Mon May 21 14:36:24 2001 +0200
@@ -17,9 +17,9 @@
 
 (*Induction on term(A) followed by induction on List *)
 val major::prems = Goal
-    "[| t: term(A);  \
-\       !!x.      [| x: A |] ==> P(Apply(x,Nil));  \
-\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  P(Apply(x,zs))  \
+    "[| t \\<in> term(A);  \
+\       !!x.      [| x \\<in> A |] ==> P(Apply(x,Nil));  \
+\       !!x z zs. [| x \\<in> A;  z \\<in> term(A);  zs: list(term(A));  P(Apply(x,zs))  \
 \                 |] ==> P(Apply(x, Cons(z,zs)))  \
 \    |] ==> P(t)";
 by (rtac (major RS term.induct) 1);
@@ -30,8 +30,8 @@
 
 (*Induction on term(A) to prove an equation*)
 val major::prems = Goal
-    "[| t: term(A);  \
-\       !!x zs. [| x: A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==> \
+    "[| t \\<in> term(A);  \
+\       !!x zs. [| x \\<in> A;  zs: list(term(A));  map(f,zs) = map(g,zs) |] ==> \
 \               f(Apply(x,zs)) = g(Apply(x,zs))  \
 \    |] ==> f(t)=g(t)";
 by (rtac (major RS term.induct) 1);
@@ -41,14 +41,14 @@
 
 (**  Lemmas to justify using "term" in other recursive type definitions **)
 
-Goalw term.defs "A<=B ==> term(A) <= term(B)";
+Goalw term.defs "A \\<subseteq> B ==> term(A) \\<subseteq> term(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (rtac term.bnd_mono 1));
 by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
 qed "term_mono";
 
 (*Easily provable by induction also*)
-Goalw (term.defs@term.con_defs) "term(univ(A)) <= univ(A)";
+Goalw (term.defs@term.con_defs) "term(univ(A)) \\<subseteq> univ(A)";
 by (rtac lfp_lowerbound 1);
 by (rtac (A_subset_univ RS univ_mono) 2);
 by Safe_tac;
@@ -58,7 +58,7 @@
 val term_subset_univ = 
     term_mono RS (term_univ RSN (2,subset_trans)) |> standard;
 
-Goal "[| t: term(A);  A <= univ(B) |] ==> t: univ(B)";
+Goal "[| t \\<in> term(A);  A \\<subseteq> univ(B) |] ==> t \\<in> univ(B)";
 by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1));
 qed "term_into_univ";
 
@@ -66,8 +66,8 @@
 (*** term_rec -- by Vset recursion ***)
 
 (*Lemma: map works correctly on the underlying list of terms*)
-Goal "[| l: list(A);  Ord(i) |] ==>  \
-\     rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
+Goal "[| l \\<in> list(A);  Ord(i) |] ==>  \
+\     rank(l)<i --> map(%z. (\\<lambda>x \\<in> Vset(i).h(x)) ` z, l) = map(h,l)";
 by (etac list.induct 1);
 by (Simp_tac 1);
 by (rtac impI 1);
@@ -78,7 +78,7 @@
 qed "map_lemma";
 
 (*Typing premise is necessary to invoke map_lemma*)
-Goal "ts: list(A) ==> \
+Goal "ts \\<in> list(A) ==> \
 \     term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
 by (rtac (term_rec_def RS def_Vrec RS trans) 1);
 by (rewrite_goals_tac term.con_defs);
@@ -87,11 +87,11 @@
 
 (*Slightly odd typing condition on r in the second premise!*)
 val major::prems = Goal
-    "[| t: term(A);                                     \
-\       !!x zs r. [| x: A;  zs: list(term(A));          \
-\                    r: list(UN t:term(A). C(t)) |]     \
+    "[| t \\<in> term(A);                                     \
+\       !!x zs r. [| x \\<in> A;  zs: list(term(A));          \
+\                    r \\<in> list(\\<Union>t \\<in> term(A). C(t)) |]     \
 \                 ==> d(x, zs, r): C(Apply(x,zs))       \
-\    |] ==> term_rec(t,d) : C(t)";
+\    |] ==> term_rec(t,d) \\<in> C(t)";
 by (rtac (major RS term.induct) 1);
 by (ftac list_CollectD 1);
 by (stac term_rec 1);
@@ -109,10 +109,10 @@
 qed "def_term_rec";
 
 val prems = Goal
-    "[| t: term(A);                                          \
-\       !!x zs r. [| x: A;  zs: list(term(A));  r: list(C) |]  \
+    "[| t \\<in> term(A);                                          \
+\       !!x zs r. [| x \\<in> A;  zs: list(term(A));  r \\<in> list(C) |]  \
 \                 ==> d(x, zs, r): C                 \
-\    |] ==> term_rec(t,d) : C";
+\    |] ==> term_rec(t,d) \\<in> C";
 by (REPEAT (ares_tac (term_rec_type::prems) 1));
 by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1);
 qed "term_rec_simple_type";
@@ -124,11 +124,11 @@
 bind_thm ("term_map", term_map_def RS def_term_rec);
 
 val prems = Goalw [term_map_def]
-    "[| t: term(A);  !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
+    "[| t \\<in> term(A);  !!x. x \\<in> A ==> f(x): B |] ==> term_map(f,t) \\<in> term(B)";
 by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1));
 qed "term_map_type";
 
-Goal "t: term(A) ==> term_map(f,t) : term({f(u). u:A})";
+Goal "t \\<in> term(A) ==> term_map(f,t) \\<in> term({f(u). u \\<in> A})";
 by (etac term_map_type 1);
 by (etac RepFunI 1);
 qed "term_map_type2";
@@ -138,7 +138,7 @@
 
 bind_thm ("term_size", term_size_def RS def_term_rec);
 
-Goalw [term_size_def] "t: term(A) ==> term_size(t) : nat";
+Goalw [term_size_def] "t \\<in> term(A) ==> term_size(t) \\<in> nat";
 by Auto_tac;
 qed "term_size_type";
 
@@ -147,7 +147,7 @@
 
 bind_thm ("reflect", reflect_def RS def_term_rec);
 
-Goalw [reflect_def] "t: term(A) ==> reflect(t) : term(A)";
+Goalw [reflect_def] "t \\<in> term(A) ==> reflect(t) \\<in> term(A)";
 by Auto_tac;
 qed "reflect_type";
 
@@ -155,7 +155,7 @@
 
 bind_thm ("preorder", preorder_def RS def_term_rec);
 
-Goalw [preorder_def] "t: term(A) ==> preorder(t) : list(A)";
+Goalw [preorder_def] "t \\<in> term(A) ==> preorder(t) \\<in> list(A)";
 by Auto_tac;
 qed "preorder_type";
 
@@ -163,7 +163,7 @@
 
 bind_thm ("postorder", postorder_def RS def_term_rec);
 
-Goalw [postorder_def] "t: term(A) ==> postorder(t) : list(A)";
+Goalw [postorder_def] "t \\<in> term(A) ==> postorder(t) \\<in> list(A)";
 by Auto_tac;
 qed "postorder_type";
 
@@ -181,17 +181,17 @@
 
 Addsimps [thm "List.map_compose"];  (*there is also TF.map_compose*)
 
-Goal "t: term(A) ==> term_map(%u. u, t) = t";
+Goal "t \\<in> term(A) ==> term_map(%u. u, t) = t";
 by (etac term_induct_eqn 1);
 by (Asm_simp_tac 1);
 qed "term_map_ident";
 
-Goal "t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
+Goal "t \\<in> term(A) ==> term_map(f, term_map(g,t)) = term_map(%u. f(g(u)), t)";
 by (etac term_induct_eqn 1);
 by (Asm_simp_tac 1);
 qed "term_map_compose";
 
-Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
+Goal "t \\<in> term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
 by (etac term_induct_eqn 1);
 by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym]) 1);
 qed "term_map_reflect";
@@ -199,17 +199,17 @@
 
 (** theorems about term_size **)
 
-Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
+Goal "t \\<in> term(A) ==> term_size(term_map(f,t)) = term_size(t)";
 by (etac term_induct_eqn 1);
 by (Asm_simp_tac 1);
 qed "term_size_term_map";
 
-Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)";
+Goal "t \\<in> term(A) ==> term_size(reflect(t)) = term_size(t)";
 by (etac term_induct_eqn 1);
 by (asm_simp_tac(simpset() addsimps [rev_map_distrib RS sym, list_add_rev]) 1);
 qed "term_size_reflect";
 
-Goal "t: term(A) ==> term_size(t) = length(preorder(t))";
+Goal "t \\<in> term(A) ==> term_size(t) = length(preorder(t))";
 by (etac term_induct_eqn 1);
 by (asm_simp_tac (simpset() addsimps [length_flat]) 1);
 qed "term_size_length";
@@ -217,7 +217,7 @@
 
 (** theorems about reflect **)
 
-Goal "t: term(A) ==> reflect(reflect(t)) = t";
+Goal "t \\<in> term(A) ==> reflect(reflect(t)) = t";
 by (etac term_induct_eqn 1);
 by (asm_simp_tac (simpset() addsimps [rev_map_distrib]) 1);
 qed "reflect_reflect_ident";
@@ -225,12 +225,12 @@
 
 (** theorems about preorder **)
 
-Goal "t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
+Goal "t \\<in> term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
 by (etac term_induct_eqn 1);
 by (asm_simp_tac (simpset() addsimps [map_flat]) 1);
 qed "preorder_term_map";
 
-Goal "t: term(A) ==> preorder(reflect(t)) = rev(postorder(t))";
+Goal "t \\<in> term(A) ==> preorder(reflect(t)) = rev(postorder(t))";
 by (etac term_induct_eqn 1);
 by (asm_simp_tac(simpset() addsimps [rev_app_distrib, rev_flat, 
 				     rev_map_distrib RS sym]) 1);

--- a/src/ZF/ex/Term.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Term.thy	Mon May 21 14:36:24 2001 +0200
@@ -12,7 +12,7 @@
   term      :: i=>i
 
 datatype
-  "term(A)" = Apply ("a: A", "l: list(term(A))")
+  "term(A)" = Apply ("a \\<in> A", "l \\<in> list(term(A))")
   monos        list_mono
 
   type_elims  "[make_elim (list_univ RS subsetD)]"

--- a/src/ZF/ex/misc.ML	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/misc.ML	Mon May 21 14:36:24 2001 +0200
@@ -10,27 +10,27 @@
 (*These two are cited in Benzmueller and Kohlhase's system description of LEO,
   CADE-15, 1998 (page 139-143) as theorems LEO could not prove.*)
 
-Goal "(X = Y Un Z) <-> (Y<=X & Z<=X & (ALL V. Y<=V & Z<=V --> X<=V))";
+Goal "(X = Y Un Z) <-> (Y \\<subseteq> X & Z \\<subseteq> X & (\\<forall>V. Y \\<subseteq> V & Z \\<subseteq> V --> X \\<subseteq> V))";
 by (blast_tac (claset() addSIs [equalityI]) 1);
 qed "";
 
 (*the dual of the previous one*)
-Goal "(X = Y Int Z) <-> (X<=Y & X<=Z & (ALL V. V<=Y & V<=Z --> V<=X))";
+Goal "(X = Y Int Z) <-> (X \\<subseteq> Y & X \\<subseteq> Z & (\\<forall>V. V \\<subseteq> Y & V \\<subseteq> Z --> V \\<subseteq> X))";
 by (blast_tac (claset() addSIs [equalityI]) 1);
 qed "";
 
 (*trivial example of term synthesis: apparently hard for some provers!*)
-Goal "a ~= b ==> a:?X & b ~: ?X";
+Goal "a \\<noteq> b ==> a:?X & b \\<notin> ?X";
 by (Blast_tac 1);
 qed "";
 
 (*Nice Blast_tac benchmark.  Proved in 0.3s; old tactics can't manage it!*)
-Goal "ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
+Goal "\\<forall>x \\<in> S. \\<forall>y \\<in> S. x \\<subseteq> y ==> \\<exists>z. S \\<subseteq> {z}";
 by (Blast_tac 1);
 qed "";
 
 (*variant of the benchmark above*)
-Goal "ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
+Goal "\\<forall>x \\<in> S. Union(S) \\<subseteq> x ==> \\<exists>z. S \\<subseteq> {z}";
 by (Blast_tac 1);
 qed "";
 
@@ -40,7 +40,7 @@
  W. Bledsoe.  A Maximal Method for Set Variables in Automatic Theorem-proving.
  In: J. Hayes and D. Michie and L. Mikulich, eds.  Machine Intelligence 9.
  Ellis Horwood, 53-100 (1979). *)
-Goal "(ALL F. {x}: F --> {y}:F) --> (ALL A. x:A --> y:A)";
+Goal "(\\<forall>F. {x}: F --> {y}:F) --> (\\<forall>A. x \\<in> A --> y \\<in> A)";
 by (Best_tac 1);
 qed "";
 
@@ -60,21 +60,21 @@
   proving conditions of rewrites such as comp_fun_apply;
   rewriting does not instantiate Vars*)
 goal Perm.thy
-    "(ALL A f B g. hom(A,f,B,g) = \
-\          {H: A->B. f:A*A->A & g:B*B->B & \
-\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
-\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
-\    (K O J) : hom(A,f,C,h)";
+    "(\\<forall>A f B g. hom(A,f,B,g) = \
+\          {H \\<in> A->B. f \\<in> A*A->A & g \\<in> B*B->B & \
+\                    (\\<forall>x \\<in> A. \\<forall>y \\<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) --> \
+\    J \\<in> hom(A,f,B,g) & K \\<in> hom(B,g,C,h) -->  \
+\    (K O J) \\<in> hom(A,f,C,h)";
 by (asm_simp_tac (simpset() setloop (K Safe_tac)) 1);
 qed "";
 
 (*This version uses meta-level rewriting, safe_tac and asm_simp_tac*)
 val [hom_def] = goal Perm.thy
     "(!! A f B g. hom(A,f,B,g) == \
-\          {H: A->B. f:A*A->A & g:B*B->B & \
-\                    (ALL x:A. ALL y:A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
-\    J : hom(A,f,B,g) & K : hom(B,g,C,h) -->  \
-\    (K O J) : hom(A,f,C,h)";
+\          {H \\<in> A->B. f \\<in> A*A->A & g \\<in> B*B->B & \
+\                    (\\<forall>x \\<in> A. \\<forall>y \\<in> A. H`(f`<x,y>) = g`<H`x,H`y>)}) ==> \
+\    J \\<in> hom(A,f,B,g) & K \\<in> hom(B,g,C,h) -->  \
+\    (K O J) \\<in> hom(A,f,C,h)";
 by (rewtac hom_def);
 by Safe_tac;
 by (Asm_simp_tac 1);
@@ -85,7 +85,7 @@
 (** A characterization of functions, suggested by Tobias Nipkow **)
 
 Goalw [Pi_def, function_def]
-    "r: domain(r)->B  <->  r <= domain(r)*B & (ALL X. r `` (r -`` X) <= X)";
+    "r \\<in> domain(r)->B  <->  r \\<subseteq> domain(r)*B & (\\<forall>X. r `` (r -`` X) \\<subseteq> X)";
 by (Best_tac 1);
 qed "";
 
@@ -119,7 +119,7 @@
     "[| (h O g O f): inj(A,A);          \
 \       (f O h O g): surj(B,B);         \
 \       (g O f O h): surj(C,C);         \
-\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
+\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
 qed "pastre1";
 
@@ -127,7 +127,7 @@
     "[| (h O g O f): surj(A,A);         \
 \       (f O h O g): inj(B,B);          \
 \       (g O f O h): surj(C,C);         \
-\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
+\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
 qed "pastre2";
 
@@ -135,7 +135,7 @@
     "[| (h O g O f): surj(A,A);         \
 \       (f O h O g): surj(B,B);         \
 \       (g O f O h): inj(C,C);          \
-\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
+\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
 qed "pastre3";
 
@@ -143,7 +143,7 @@
     "[| (h O g O f): surj(A,A);         \
 \       (f O h O g): inj(B,B);          \
 \       (g O f O h): inj(C,C);          \
-\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
+\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
 qed "pastre4";
 
@@ -151,7 +151,7 @@
     "[| (h O g O f): inj(A,A);          \
 \       (f O h O g): surj(B,B);         \
 \       (g O f O h): inj(C,C);          \
-\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
+\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
 qed "pastre5";
 
@@ -159,16 +159,16 @@
     "[| (h O g O f): inj(A,A);          \
 \       (f O h O g): inj(B,B);          \
 \       (g O f O h): surj(C,C);         \
-\       f: A->B;  g: B->C;  h: C->A |] ==> h: bij(C,A)";
+\       f \\<in> A->B;  g \\<in> B->C;  h \\<in> C->A |] ==> h \\<in> bij(C,A)";
 by (REPEAT (resolve_tac (IntI :: pastre_facts prems) 1));
 qed "pastre6";
 
 (** Yet another example... **)
 
 goal Perm.thy
-    "(lam Z:Pow(A+B). <{x:A. Inl(x):Z}, {y:B. Inr(y):Z}>) \
-\    : bij(Pow(A+B), Pow(A)*Pow(B))";
-by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
+    "(\\<lambda>Z \\<in> Pow(A+B). <{x \\<in> A. Inl(x):Z}, {y \\<in> B. Inr(y):Z}>) \
+\    \\<in> bij(Pow(A+B), Pow(A)*Pow(B))";
+by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x \\<in> X} Un {Inr(y).y \\<in> Y}")] 
     lam_bijective 1);
 (*Auto_tac no longer proves it*)
 by Auto_tac;
@@ -177,9 +177,9 @@
 
 (*As a special case, we have  bij(Pow(A*B), A -> Pow B)  *)
 goal Perm.thy
-    "(lam r:Pow(Sigma(A,B)). lam x:A. r``{x}) \
-\    : bij(Pow(Sigma(A,B)), PROD x:A. Pow(B(x)))";
-by (res_inst_tac [("d", "%f. UN x:A. UN y:f`x. {<x,y>}")] lam_bijective 1);
+    "(\\<lambda>r \\<in> Pow(Sigma(A,B)). \\<lambda>x \\<in> A. r``{x}) \
+\    \\<in> bij(Pow(Sigma(A,B)), \\<Pi>x \\<in> A. Pow(B(x)))";
+by (res_inst_tac [("d", "%f. \\<Union>x \\<in> A. \\<Union>y \\<in> f`x. {<x,y>}")] lam_bijective 1);
 by (blast_tac (claset() addDs [apply_type]) 2);
 by (blast_tac (claset() addIs [lam_type]) 1);
 by (ALLGOALS Asm_simp_tac);

author	paulson
	Mon, 21 May 2001 14:36:24 +0200
changeset 11316	b4e71bd751e4
parent 11315	fbca0f74bcef
child 11317	7f9e4c389318

src/ZF/ex/Acc.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Acc.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/BT.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/BT.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Brouwer.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Brouwer.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/CoUnit.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/CoUnit.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Comb.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Comb.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Commutation.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Commutation.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Data.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Data.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Enum.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/LList.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/LList.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Limit.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Limit.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/ListN.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/ListN.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Mutil.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Mutil.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/NatSum.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Ntree.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Ntree.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Primes.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Primes.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Primrec.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Primrec.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Primrec_defs.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Primrec_defs.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/PropLog.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/PropLog.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Ramsey.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Ramsey.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Rmap.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Rmap.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/TF.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/TF.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Term.ML		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/Term.thy		file \| annotate \| diff \| comparison \| revisions
src/ZF/ex/misc.ML		file \| annotate \| diff \| comparison \| revisions