# HG changeset patch
# User paulson
# Date 994166957 -7200
# Node ID 2eeaa1077b7373a65ddcfc0c68b3c8e7b540c5ed
# Parent  e88c2c89f98ed5d79f76e4b95a245110ae1a1e30
better treatment of restrict (lam)

diff -r e88c2c89f98e -r 2eeaa1077b73 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Tue Jul 03 15:28:24 2001 +0200
+++ b/src/HOL/Fun.ML	Tue Jul 03 15:29:17 2001 +0200
@@ -144,7 +144,7 @@
 (*** inj_on f A: f is one-to-one over A ***)
 
 val prems = Goalw [inj_on_def]
-    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
+    "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A";
 by (blast_tac (claset() addIs prems) 1);
 qed "inj_onI";
 bind_thm ("injI", inj_onI);                  (*for compatibility*)
@@ -577,17 +577,10 @@
 by (asm_simp_tac (simpset() addsimps prems) 1);
 qed "restrictI";
 
-Goal "x: A ==> (lam y: A. f y) x = f x";
+Goal "(lam y: A. f y) x = (if x : A then f x else (@ y. True))";
 by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
-qed "restrict_apply1";
-
-Goal "[| x: A; f : A funcset B |] ==> (lam y: A. f y) x : B";
-by (asm_full_simp_tac (simpset() addsimps [restrict_apply1,Pi_def]) 1);
-qed "restrict_apply1_mem";
-
-Goal "x ~: A ==> (lam y: A. f y) x =  (@ y. True)";
-by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
-qed "restrict_apply2";
+qed "restrict_apply";
+Addsimps [restrict_apply];
 
 val prems = Goal
     "(!!x. x: A ==> f x = g x) ==> (lam x: A. f x) = (lam x: A. g x)";
@@ -612,18 +605,17 @@
 by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
 qed "Inv_funcset";
 
-
-Goal "[| f: A funcset B;  inj_on f A;  f ` A = B;  x: A |] \
-\     ==> (lam y: B. (Inv A f) y) (f x) = x";
-by (asm_simp_tac (simpset() addsimps [restrict_apply1, funcset_mem]) 1);
+Goal "[| inj_on f A;  f: A funcset (f`A);  x : A |] \
+\     ==> Inv A f (f x) = x";
 by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
 by (rtac someI2 1);
 by Auto_tac;
 qed "Inv_f_f";
 
+(*a strange theorem, but so is f_inv_f*)
 Goal "[| f: A funcset B;  f ` A = B;  x: B |] \
 \     ==> f ((lam y: B. (Inv A f y)) x) = x";
-by (asm_simp_tac (simpset() addsimps [Inv_def, restrict_apply1]) 1);
+by (asm_simp_tac (simpset() addsimps [Inv_def]) 1);
 by (fast_tac (claset() addIs [someI2]) 1);
 qed "f_Inv_f";
 
@@ -633,7 +625,8 @@
 by (blast_tac (claset() addIs [funcset_compose, Inv_funcset]) 1);
 by (blast_tac (claset() addIs [restrict_in_funcset]) 1);
 by (asm_simp_tac
-    (simpset() addsimps [restrict_apply1, compose_def, Inv_f_f]) 1);
+    (simpset() addsimps [compose_def, Inv_f_f]) 1);
+by Auto_tac;
 qed "compose_Inv_id";
 
 
diff -r e88c2c89f98e -r 2eeaa1077b73 src/HOL/ex/PiSets.ML
--- a/src/HOL/ex/PiSets.ML	Tue Jul 03 15:28:24 2001 +0200
+++ b/src/HOL/ex/PiSets.ML	Tue Jul 03 15:29:17 2001 +0200
@@ -8,12 +8,11 @@
 (*** Bijection between Pi in terms of => and Pi in terms of Sigma ***)
 Goal "f: Pi A B ==> PiBij A B f <= Sigma A B";
 by (auto_tac (claset(),
-	      simpset() addsimps [PiBij_def,Pi_def,restrict_apply1]));
+	      simpset() addsimps [PiBij_def,Pi_def]));
 qed "PiBij_subset_Sigma";
 
 Goal "f: Pi A B ==> (! x: A. (?! y. (x, y): (PiBij A B f)))";
-by (auto_tac (claset(),
-	      simpset() addsimps [PiBij_def,restrict_apply1]));
+by (auto_tac (claset(), simpset() addsimps [PiBij_def]));
 qed "PiBij_unique";
 
 Goal "f: Pi A B ==> PiBij A B f : Graph A B";
@@ -31,51 +30,38 @@
 by (rtac Pi_extensionality 1);			
 by (assume_tac 1);
 by (assume_tac 1);
-by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps [PiBij_def,restrict_apply1]) 1);
+by (asm_full_simp_tac (simpset() addsimps [PiBij_def]) 1);
 by (Blast_tac 1);
 qed "inj_PiBij";
 
 
+Goal "x \\<in> Graph A B \\<Longrightarrow> (lam a:A. SOME y. (a, y) \\<in> x) \\<in> Pi A B";
+by (rtac restrictI 1);
+by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 1);
+ by (force_tac (claset(), simpset() addsimps [Graph_def]) 1);
+by (full_simp_tac (simpset() addsimps [Graph_def]) 1);
+by (stac some_equality 1);
+  by (assume_tac 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
+qed "in_Graph_imp_in_Pi";
 
 Goal "PiBij A B ` (Pi A B) = Graph A B";
 by (rtac equalityI 1);
-by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
+by (force_tac (claset(), simpset() addsimps [PiBij_in_Graph]) 1);
 by (rtac subsetI 1);
-by (asm_full_simp_tac (simpset() addsimps [image_def]) 1);
-by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
- by (rtac restrictI 2);
- by (res_inst_tac [("P", "%xa. (a, xa) : x")] ex1E 2);
-  by (force_tac (claset(), simpset() addsimps [Graph_def]) 2);
- by (full_simp_tac (simpset() addsimps [Graph_def]) 2);
-  by (stac some_equality 2);
-   by (assume_tac 2);
-  by (Blast_tac 2);
- by (Blast_tac 2);
+by (rtac image_eqI 1); 
+by (etac in_Graph_imp_in_Pi 2); 
 (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
-by (full_simp_tac (simpset() addsimps [PiBij_def,Graph_def]) 1);
-by (stac restrict_apply1 1);
- by (rtac restrictI 1);
- by (blast_tac (claset() addSDs [[some_eq_ex, ex1_implies_ex] MRS iffD2]) 1);
-(** LEVEL 17 **)
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (split_all_tac 1);
-by (subgoal_tac "a: A" 1);
-by (Blast_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
-(*Blast_tac: PROOF FAILED for depth 5*)
-by (fast_tac (claset() addSIs [some1_equality RS sym]) 1);
-(* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [restrict_apply1]) 1);
+by (asm_simp_tac (simpset() addsimps [in_Graph_imp_in_Pi, PiBij_def]) 1);
+by (auto_tac (claset(), simpset() addsimps [some1_equality, Graph_def])); 
 by (fast_tac (claset() addIs [someI2]) 1);
 qed "surj_PiBij";
 
 Goal "f: Pi A B ==> \
 \     (lam y: Graph A B. (Inv (Pi A B)(PiBij A B)) y)(PiBij A B f) = f";
-by (asm_simp_tac
-    (simpset() addsimps [Inv_f_f, PiBij_func, inj_PiBij, surj_PiBij]) 1);
+by (asm_simp_tac (simpset() addsimps [Inv_f_f, PiBij_in_Graph, PiBij_func, 
+                                      inj_PiBij, surj_PiBij]) 1);
 qed "PiBij_bij1";
 
 Goal "[| f: Graph A B  |] ==> \
@@ -84,4 +70,3 @@
 by (asm_full_simp_tac (simpset() addsimps [surj_PiBij]) 1);
 by (assume_tac 1);
 qed "PiBij_bij2";
-
diff -r e88c2c89f98e -r 2eeaa1077b73 src/HOL/ex/Tarski.ML
--- a/src/HOL/ex/Tarski.ML	Tue Jul 03 15:28:24 2001 +0200
+++ b/src/HOL/ex/Tarski.ML	Tue Jul 03 15:29:17 2001 +0200
@@ -34,57 +34,44 @@
 by (simp_tac (simpset() addsimps PO_simp) 1);
 qed "PartialOrderE3";
 
-Goal "[| refl A r; x: A|] ==> (x, x): r";
+Goal "[| refl A r; x \\<in> A|] ==> (x, x) \\<in> r";
 by (afs [refl_def] 1);
 qed "reflE";
 (* Interesting: A and r don't get bound because the proof doesn't use
    locale rules 
-val reflE = "[| refl ?A ?r; ?x : ?A |] ==> (?x, ?x) : ?r" *)
+val reflE = "[| refl ?A ?r; ?x \\<in> ?A |] ==> (?x, ?x) \\<in> ?r" *)
 
-Goal "[| antisym r; (a, b): r; (b, a): r |] ==> a = b";
+Goal "[| antisym r; (a, b) \\<in> r; (b, a) \\<in> r |] ==> a = b";
 by (afs [antisym_def] 1);
 qed "antisymE";
 
-Goalw [trans_def] "[| trans r; (a, b): r; (b, c): r|] ==> (a,c): r";
+Goalw [trans_def] "[| trans r; (a, b) \\<in> r; (b, c) \\<in> r|] ==> (a,c) \\<in> r";
 by (Fast_tac 1);
 qed "transE";
 
-Goal "[| monotone f A r;  x: A; y: A; (x, y): r |] ==> (f x, f y): r";
+Goal "[| monotone f A r;  x \\<in> A; y \\<in> A; (x, y) \\<in> r |] ==> (f x, f y) \\<in> r";
 by (afs [monotone_def] 1);
 qed "monotoneE";
 
-Goal "S <= A ==> (| pset = S, order = induced S r |): PartialOrder";
+Goal "S <= A ==> (| pset = S, order = induced S r |) \\<in> PartialOrder";
 by (simp_tac (simpset() addsimps [PartialOrder_def]) 1);
-by (Step_tac 1);
+by Auto_tac; 
 (* refl *)
 by (afs [refl_def,induced_def] 1);
-by (rtac conjI 1);
-by (Fast_tac 1);
-by (rtac ballI 1);
-by (rtac reflE 1);
-by (rtac PartialOrderE1 1);
-by (Fast_tac 1);
+by (blast_tac (claset() addIs [PartialOrderE1 RS reflE]) 1); 
 (* antisym *)
 by (afs [antisym_def,induced_def] 1);
-by (Step_tac 1);
-by (rtac antisymE 1);
-by (assume_tac 2);
-by (assume_tac 2);
-by (rtac PartialOrderE2 1);
+by (blast_tac (claset() addIs [PartialOrderE2 RS antisymE]) 1); 
 (* trans *)
 by (afs [trans_def,induced_def] 1);
-by (Step_tac 1);
-by (rtac transE 1);
-by (assume_tac 2);
-by (assume_tac 2);
-by (rtac PartialOrderE3 1);
+by (blast_tac (claset() addIs [PartialOrderE3 RS transE]) 1); 
 qed "po_subset_po";
 
-Goal "[| (x, y): induced S r; S <= A |] ==> (x, y): r";
+Goal "[| (x, y) \\<in> induced S r; S <= A |] ==> (x, y) \\<in> r";
 by (afs [induced_def] 1);
 qed "indE";
 
-Goal "[| (x, y): r; x: S; y: S |] ==> (x, y): induced S r";
+Goal "[| (x, y) \\<in> r; x \\<in> S; y \\<in> S |] ==> (x, y) \\<in> induced S r";
 by (afs [induced_def] 1);
 qed "indI";
 
@@ -113,18 +100,18 @@
 by (afs [islub_def,isglb_def,dual_def,converse_def] 1);
 qed "islub_dual_isglb";
 
-Goal "dual cl : PartialOrder";
+Goal "dual cl \\<in> PartialOrder";
 by (simp_tac (simpset() addsimps [PartialOrder_def, dual_def]) 1);
 by (afs [simp_PO,refl_converse,trans_converse,antisym_converse] 1);
 qed "dualPO";
 
-Goal "! S. (S <= A -->( ? L. islub S (| pset = A, order = r|) L)) \
-\     ==> ! S. (S <= A --> (? G. isglb S (| pset = A, order = r|) G))";
+Goal "\\<forall>S. (S <= A -->( \\<exists>L. islub S (| pset = A, order = r|) L)) \
+\     ==> \\<forall>S. (S <= A --> (\\<exists>G. isglb S (| pset = A, order = r|) G))";
 by (Step_tac 1);
 by (res_inst_tac
-    [("x"," lub {y. y: A & (! k: S. (y, k): r)}(|pset = A, order = r|)")] 
+    [("x"," lub {y. y \\<in> A & (\\<forall>k \\<in> S. (y, k) \\<in> r)}(|pset = A, order = r|)")] 
     exI 1);
-by (dres_inst_tac [("x","{y. y: A & (! k: S. (y,k): r)}")] spec 1);
+by (dres_inst_tac [("x","{y. y \\<in> A & (\\<forall>k \\<in> S. (y,k) \\<in> r)}")] spec 1);
 by (dtac mp 1);
 by (Fast_tac 1);
 by (afs [islub_lub, isglb_def] 1);
@@ -147,11 +134,11 @@
 
 val CompleteLatticeE1 = CL_subset_PO RS subsetD;
 
-Goal "! S.  S <= A --> (? L. islub S cl L)";
+Goal "\\<forall>S.  S <= A --> (\\<exists>L. islub S cl L)";
 by (simp_tac (simpset() addsimps PO_simp) 1);
 qed "CompleteLatticeE2";
 
-Goal "! S.  S <= A --> (? G. isglb S cl G)";
+Goal "\\<forall>S.  S <= A --> (\\<exists>G. isglb S cl G)";
 by (simp_tac (simpset() addsimps PO_simp) 1);
 qed "CompleteLatticeE3";
 
@@ -169,12 +156,12 @@
 by (afs (PO_simp) 1);
 qed "CompleteLatticeE13";
 
-Goal "[| po : PartialOrder; (! S. S <= po.<A> --> (? L. islub S po L));\
-\  (! S. S <= po.<A> --> (? G. isglb S po G))|] ==> po: CompleteLattice";
+Goal "[| po \\<in> PartialOrder; (\\<forall>S. S <= po.<A> --> (\\<exists>L. islub S po L));\
+\  (\\<forall>S. S <= po.<A> --> (\\<exists>G. isglb S po G))|] ==> po \\<in> CompleteLattice";
 by (afs [CompleteLattice_def] 1);
 qed "CompleteLatticeI";
 
-Goal "dual cl : CompleteLattice";
+Goal "dual cl \\<in> CompleteLattice";
 by (simp_tac (simpset() addsimps [CompleteLattice_def,dual_def]) 1);
 by (fold_goals_tac [dual_def]);
 by (simp_tac (simpset() addsimps [islub_dual_isglb RS sym,
@@ -186,7 +173,7 @@
 by (simp_tac (simpset() addsimps [dual_def]) 1);
 qed "dualA_iff";
 
-Goal "((x, y): (dual cl.<r>)) = ((y, x): cl.<r>)";
+Goal "((x, y) \\<in> (dual cl.<r>)) = ((y, x) \\<in> cl.<r>)";
 by (simp_tac (simpset() addsimps [dual_def]) 1);
 qed "dualr_iff";
 
@@ -194,37 +181,37 @@
 by (afs [monotone_def,dualA_iff,dualr_iff] 1);
 qed "monotone_dual";
 
-Goal "[| x: A; y: A|] ==> interval r x y = interval (dual cl.<r>) y x";
+Goal "[| x \\<in> A; y \\<in> A|] ==> interval r x y = interval (dual cl.<r>) y x";
 by (simp_tac (simpset() addsimps [interval_def,dualr_iff]) 1);
 by (fold_goals_tac [thm "r_def"]);
 by (Fast_tac 1);
 qed "interval_dual";
 
-Goal "[| trans r; interval r a b ~= {} |] ==> (a, b): r";
+Goal "[| trans r; interval r a b \\<noteq> {} |] ==> (a, b) \\<in> r";
 by (afs [interval_def] 1);
 by (rewtac trans_def);
 by (Blast_tac 1);
 qed "interval_not_empty";
 
-Goal "x: interval r a b ==> (a, x): r";
+Goal "x \\<in> interval r a b ==> (a, x) \\<in> r";
 by (afs [interval_def] 1);
 qed "intervalE1";
 
-Goal "[| a: A; b: A; interval r a b ~= {} |] ==> a: interval r a b";
+Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {} |] ==> a \\<in> interval r a b";
 by (simp_tac (simpset() addsimps [interval_def]) 1);
 by (afs [PartialOrderE3,interval_not_empty] 1);
 by (afs [PartialOrderE1 RS reflE] 1);
 qed "left_in_interval";
 
-Goal "[| a: A; b: A; interval r a b ~= {} |] ==> b: interval r a b";
+Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {} |] ==> b \\<in> interval r a b";
 by (simp_tac (simpset() addsimps [interval_def]) 1);
 by (afs [PartialOrderE3,interval_not_empty] 1);
 by (afs [PartialOrderE1 RS reflE] 1);
 qed "right_in_interval";
 
-Goal "[| (| pset = A, order = r |) : PartialOrder;\
-\        ! S. S <= A --> (? L. islub S (| pset = A, order = r |)  L) |] \
-\   ==> (| pset = A, order = r |) : CompleteLattice";
+Goal "[| (| pset = A, order = r |) \\<in> PartialOrder;\
+\        \\<forall>S. S <= A --> (\\<exists>L. islub S (| pset = A, order = r |)  L) |] \
+\   ==> (| pset = A, order = r |) \\<in> CompleteLattice";
 by (afs [CompleteLatticeI, Rdual] 1);
 qed "CompleteLatticeI_simp";
 
@@ -233,11 +220,11 @@
 by (afs [sublattice_def, CompleteLattice_def, thm "A_def"] 1);
 qed "sublatticeE1";
 
-Goal "S <<= cl  ==> (| pset = S, order = induced S r |) : CompleteLattice";
+Goal "S <<= cl  ==> (| pset = S, order = induced S r |) \\<in> CompleteLattice";
 by (afs ([sublattice_def, CompleteLattice_def] @ PO_simp) 1);
 qed "sublatticeE2";
 
-Goal "[| S <= A; (| pset = S, order = induced S r |) : CompleteLattice |] ==> S <<= cl";
+Goal "[| S <= A; (| pset = S, order = induced S r |) \\<in> CompleteLattice |] ==> S <<= cl";
 by (afs ([sublattice_def] @ PO_simp) 1);
 qed "sublatticeI";
 
@@ -245,30 +232,10 @@
 Goal "[| S <= A; islub S cl x; islub S cl L|] ==> x = L";
 by (rtac antisymE 1); 
 by (rtac CompleteLatticeE12 1);
-by (rewtac islub_def);
-by (rotate_tac ~1 1);
-by (etac conjE 1);
-by (dtac conjunct2 1);
-by (dtac conjunct1 1);
-by (dtac conjunct2 1);
-by (rotate_tac ~1 1);
-by (dres_inst_tac [("x","L")] bspec 1);
-by (assume_tac 1);
-by (fold_goals_tac [thm "r_def"]);
-by (etac mp 1);
-by (assume_tac 1);
-(* (L, x) : (cl .<r>) *)
-by (rotate_tac ~1 1);
-by (etac conjE 1);
-by (rotate_tac ~1 1);
-by (dtac conjunct2 1);
-by (dtac bspec 1);
-by (etac conjunct1 1);
-by (etac mp 1);
-by (etac (conjunct2 RS conjunct1) 1);
+by (auto_tac (claset(), simpset() addsimps [islub_def, thm "r_def"])); 
 qed "lub_unique";
 
-Goal "[| S <= A |] ==> ! x: S. (x,lub S cl): r";
+Goal "[| S <= A |] ==> \\<forall>x \\<in> S. (x,lub S cl) \\<in> r";
 by (rtac exE 1);
 by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
 by (assume_tac 1);
@@ -285,7 +252,7 @@
 by (afs [islub_def,thm "r_def"] 1);
 qed "lubE1";
 
-Goal "[| S <= A; L: A; ! x: S. (x,L): r |] ==> (lub S cl, L): r";
+Goal "[| S <= A; L \\<in> A; \\<forall>x \\<in> S. (x,L) \\<in> r |] ==> (lub S cl, L) \\<in> r";
 by (rtac exE 1);
 by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
 by (assume_tac 1);
@@ -310,7 +277,7 @@
 by (assume_tac 1);
 qed "lubE2";
 
-Goal "[| S <= A |] ==> lub S cl : A";  
+Goal "[| S <= A |] ==> lub S cl \\<in> A";  
 by (rtac exE 1);
 by (rtac (CompleteLatticeE2 RS spec RS mp) 1);
 by (assume_tac 1);
@@ -324,8 +291,8 @@
 by (assume_tac 1);
 qed "lub_in_lattice";
 
-Goal "[| S <= A; L: A; ! x: S. (x,L): r;\
-\ ! z: A. (! y: S. (y,z): r) --> (L,z): r |] ==> L = lub S cl";
+Goal "[| S <= A; L \\<in> A; \\<forall>x \\<in> S. (x,L) \\<in> r;\
+\ \\<forall>z \\<in> A. (\\<forall>y \\<in> S. (y,z) \\<in> r) --> (L,z) \\<in> r |] ==> L = lub S cl";
 by (rtac lub_unique 1);
 by (assume_tac 1);
 by (afs ([islub_def] @ PO_simp) 1);
@@ -341,30 +308,30 @@
 by (afs ([lubI, islub_def] @ PO_simp) 1);
 qed "lubIa";
 
-Goal "islub S cl L ==> L : A";
+Goal "islub S cl L ==> L \\<in> A";
 by (afs [islub_def, thm "A_def"] 1);
 qed "islub_in_lattice";
 
-Goal "islub S cl L ==> ! y: S. (y, L): r";
+Goal "islub S cl L ==> \\<forall>y \\<in> S. (y, L) \\<in> r";
 by (afs [islub_def, thm "r_def"] 1);
 qed "islubE1";
 
 Goal "[| islub S cl L; \
-\      z: A; ! y: S. (y, z): r|] ==> (L, z): r";
+\      z \\<in> A; \\<forall>y \\<in> S. (y, z) \\<in> r|] ==> (L, z) \\<in> r";
 by (afs ([islub_def] @ PO_simp) 1);
 qed "islubE2";
 
-Goal "[| S <= A |] ==> ? L. islub S cl L";
+Goal "[| S <= A |] ==> \\<exists>L. islub S cl L";
 by (afs [thm "A_def"] 1);
 qed "islubE";
 
-Goal "[| L: A; ! y: S. (y, L): r; \
-\     (!z: A. (! y: S. (y, z):r) --> (L, z): r)|] ==> islub S cl L";
+Goal "[| L \\<in> A; \\<forall>y \\<in> S. (y, L) \\<in> r; \
+\     (\\<forall>z \\<in> A. (\\<forall>y \\<in> S. (y, z):r) --> (L, z) \\<in> r)|] ==> islub S cl L";
 by (afs ([islub_def] @ PO_simp) 1);
 qed "islubI";
 
 (* glb *)
-Goal "S <= A ==> glb S cl : A";  
+Goal "S <= A ==> glb S cl \\<in> A";  
 by (stac glb_dual_lub 1);
 by (afs [thm "A_def"] 1);
 by (rtac (dualA_iff RS subst) 1);
@@ -373,7 +340,7 @@
 by (afs [dualA_iff] 1);
 qed "glb_in_lattice";
 
-Goal "S <= A ==> ! x: S. (glb S cl, x): r";
+Goal "S <= A ==> \\<forall>x \\<in> S. (glb S cl, x) \\<in> r";
 by (stac glb_dual_lub 1);
 by (rtac ballI 1);
 by (afs [thm "r_def"] 1);
@@ -384,7 +351,7 @@
 by (assume_tac 1);
 qed "glbE1";
 
-(* Reduce the sublattice property by using substructural properties! *)
+(* Reduce the sublattice property by using substructural properties\\<forall>*)
 (* abandoned see Tarski_4.ML *)
 
 Open_locale "CLF";
@@ -392,7 +359,7 @@
 val simp_CLF = simplify (simpset() addsimps [CLF_def]) (thm "f_cl");
 Addsimps [simp_CLF, thm "f_cl"];
 
-Goal "f : A funcset A";
+Goal "f \\<in> A funcset A";
 by (simp_tac (simpset() addsimps [thm "A_def"]) 1);
 qed "CLF_E1";
 
@@ -400,7 +367,7 @@
 by (simp_tac (simpset() addsimps PO_simp) 1);
 qed "CLF_E2";
 
-Goal "f : CLF `` {cl} ==> f : CLF `` {dual cl}";
+Goal "f \\<in> CLF `` {cl} ==> f \\<in> CLF `` {dual cl}";
 by (afs [CLF_def, CL_dualCL, monotone_dual] 1); 
 by (afs [dualA_iff] 1);
 qed "CLF_dual";
@@ -411,36 +378,30 @@
 by (Fast_tac 1);
 qed "fixfE1";
 
-Goal "x: P ==> f x = x";
+Goal "x \\<in> P ==> f x = x";
 by (afs [thm "P_def", fix_def] 1);
 qed "fixfE2";
 
-Goal "[| A <= B; x: fix (lam y: A. f y) A |] ==> x: fix f B";
+Goal "[| A <= B; x \\<in> fix (lam y: A. f y) A |] ==> x \\<in> fix f B";
 by (forward_tac [export fixfE2] 1);
 by (dtac ((export fixfE1) RS subsetD) 1);
-by (afs [fix_def] 1);
-by (rtac conjI 1);
-by (Fast_tac 1);
-by (res_inst_tac [("P","% y. f x = y")] subst 1);
-by (assume_tac 1);
-by (rtac sym 1);
-by (etac restrict_apply1 1);
+by (asm_full_simp_tac (simpset() addsimps [fix_def, subsetD]) 1); 
 qed "fixf_subset";
 
 (* lemmas for Tarski, lub *)
-Goal "H = {x. (x, f x) : r & x : A} ==> (lub H cl, f (lub H cl)) : r";
+Goal "H = {x. (x, f x) \\<in> r & x \\<in> A} ==> (lub H cl, f (lub H cl)) \\<in> r";
 by (rtac lubE2 1);
 by (Fast_tac 1);
 by (rtac (CLF_E1 RS funcset_mem) 1);
 by (rtac lub_in_lattice 1);
 by (Fast_tac 1);
-(* ! x:H. (x, f (lub H r)) : r *)
+(* \\<forall>x:H. (x, f (lub H r)) \\<in> r *)
 by (rtac ballI 1);
 by (rtac transE 1);
 by (rtac CompleteLatticeE13 1);
-(* instantiates (x, ???z): cl.<r> to (x, f x), because of the def of H *)
+(* instantiates (x, ???z) \\<in> cl.<r> to (x, f x), because of the def of H *)
 by (Fast_tac 1);
-(* so it remains to show (f x, f (lub H cl)) : r *)
+(* so it remains to show (f x, f (lub H cl)) \\<in> r *)
 by (res_inst_tac [("f","f")] monotoneE 1);
 by (rtac CLF_E2 1);
 by (Fast_tac 1);
@@ -451,7 +412,7 @@
 by (assume_tac 1);
 qed "lubH_le_flubH";
 
-Goal "[|  H = {x. (x, f x) : r & x : A} |] ==> (f (lub H cl), lub H cl) : r";
+Goal "[|  H = {x. (x, f x) \\<in> r & x \\<in> A} |] ==> (f (lub H cl), lub H cl) \\<in> r";
 by (rtac (lubE1 RS bspec) 1);
 by (Fast_tac 1);
 by (res_inst_tac [("t","H")] ssubst 1);
@@ -471,7 +432,7 @@
 by (Fast_tac 1);
 qed "flubH_le_lubH";
 
-Goal "H = {x. (x, f x): r & x : A} ==> lub H cl : P";
+Goal "H = {x. (x, f x) \\<in> r & x \\<in> A} ==> lub H cl \\<in> P";
 by (simp_tac (simpset() addsimps [thm "P_def", fix_def]) 1);
 by (rtac conjI 1);
 by (rtac lub_in_lattice 1);
@@ -482,7 +443,7 @@
 by (afs [lubH_le_flubH] 1);
 qed "lubH_is_fixp";
 
-Goal "[| H = {x. (x, f x) : r & x : A};  x: P |] ==> x: H";
+Goal "[| H = {x. (x, f x) \\<in> r & x \\<in> A};  x \\<in> P |] ==> x \\<in> H";
 by (etac ssubst 1);
 by (Simp_tac 1);
 by (rtac conjI 1);
@@ -494,7 +455,7 @@
 by (etac (fixfE1 RS subsetD) 1);
 qed "fix_in_H";
 
-Goal "H = {x. (x, f x) : r & x : A} ==> ! x: P. (x, lub H cl) : r";
+Goal "H = {x. (x, f x) \\<in> r & x \\<in> A} ==> \\<forall>x \\<in> P. (x, lub H cl) \\<in> r";
 by (rtac ballI 1);
 by (rtac (lubE1 RS bspec) 1);
 by (Fast_tac 1);
@@ -502,7 +463,7 @@
 by (REPEAT (atac 1));
 qed "fixf_le_lubH";
 
-Goal "H = {x. (x, f x) : r & x : A} ==> ! L. (! y: P. (y,L): r) --> (lub H cl, L): r";
+Goal "H = {x. (x, f x) \\<in> r & x \\<in> A} ==> \\<forall>L. (\\<forall>y \\<in> P. (y,L) \\<in> r) --> (lub H cl, L) \\<in> r";
 by (rtac allI 1);
 by (rtac impI 1);
 by (etac bspec 1);
@@ -511,7 +472,7 @@
 qed "lubH_least_fixf";
 
 (* Tarski fixpoint theorem 1, first part *)
-Goal "lub P cl = lub {x. (x, f x) : r & x : A} cl";
+Goal "lub P cl = lub {x. (x, f x) \\<in> r & x \\<in> A} cl";
 by (rtac sym 1);
 by (rtac lubI 1);
 by (rtac fixfE1 1);
@@ -522,7 +483,7 @@
 qed "T_thm_1_lub";
 
 (* Tarski for glb *)
-Goal "H = {x. (f x, x): r & x : A} ==> glb H cl : P";
+Goal "H = {x. (f x, x) \\<in> r & x \\<in> A} ==> glb H cl \\<in> P";
 by (full_simp_tac 
     (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1);
 by (rtac (dualA_iff RS subst) 1);
@@ -531,7 +492,7 @@
 by (afs [dualr_iff, dualA_iff] 1);
 qed "glbH_is_fixp";
 
-Goal "glb P cl = glb {x. (f x, x): r & x : A} cl";
+Goal "glb P cl = glb {x. (f x, x) \\<in> r & x \\<in> A} cl";
 by (simp_tac (simpset() addsimps [glb_dual_lub, thm "P_def"] @ PO_simp) 1);
 by (rtac (dualA_iff RS subst) 1);
 by (rtac (CL_dualCL RS (export T_thm_1_lub) RS ssubst) 1);
@@ -544,49 +505,46 @@
 by (afs [refl_def] 1);
 qed "reflE1";
 
-Goal "(x, y): r ==> x: A";
+Goal "(x, y) \\<in> r ==> x \\<in> A";
 by (rtac SigmaD1 1);
 by (rtac (reflE1 RS subsetD) 1);
 by (rtac CompleteLatticeE11 1);
 by (assume_tac 1);
 qed "rel_imp_elem";
 
-Goal "[| a: A; b: A |] ==> interval r a b <= A";
+Goal "[| a \\<in> A; b \\<in> A |] ==> interval r a b <= A";
 by (simp_tac (simpset() addsimps [interval_def]) 1);
-by (rtac subsetI 1);
-by (rtac rel_imp_elem 1);
-by (dtac CollectD 1);
-by (etac conjunct2 1);
+by (blast_tac (claset() addIs [rel_imp_elem]) 1); 
 qed "interval_subset";
 
-Goal "[| (a, x): r; (x, b): r |] ==> x: interval r a b";
+Goal "[| (a, x) \\<in> r; (x, b) \\<in> r |] ==> x \\<in> interval r a b";
 by (afs [interval_def] 1);
 qed "intervalI";
 
-Goalw [interval_def] "[| S <= interval r a b; x: S |] ==> (a, x): r";
+Goalw [interval_def] "[| S <= interval r a b; x \\<in> S |] ==> (a, x) \\<in> r";
 by (Fast_tac 1);
 qed "interval_lemma1";
 
-Goalw [interval_def] "[| S <= interval r a b; x: S |] ==> (x, b): r";
+Goalw [interval_def] "[| S <= interval r a b; x \\<in> S |] ==> (x, b) \\<in> r";
 by (Fast_tac 1);
 qed "interval_lemma2";
 
-Goal "[| S <= A; S ~= {};\
-\        ! x: S. (a,x): r; ! y: S. (y, L): r |] ==> (a,L): r";
+Goal "[| S <= A; S \\<noteq> {};\
+\        \\<forall>x \\<in> S. (a,x) \\<in> r; \\<forall>y \\<in> S. (y, L) \\<in> r |] ==> (a,L) \\<in> r";
 by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1);
 qed "a_less_lub";
 
-Goal "[| S <= A; S ~= {};\
-\        ! x: S. (x,b): r; ! y: S. (G, y): r |] ==> (G,b): r";
+Goal "[| S <= A; S \\<noteq> {};\
+\        \\<forall>x \\<in> S. (x,b) \\<in> r; \\<forall>y \\<in> S. (G, y) \\<in> r |] ==> (G,b) \\<in> r";
 by (blast_tac (claset() addIs [transE, PartialOrderE3]) 1);
 qed "glb_less_b";
 
-Goal "[| a : A; b : A; S <= interval r a b |]==> S <= A";
+Goal "[| a \\<in> A; b \\<in> A; S <= interval r a b |]==> S <= A";
 by (afs [interval_subset RSN(2, subset_trans)] 1);
 qed "S_intv_cl";
 
-Goal "[| a : A; b: A; S <= interval r a b; \
-\      S ~= {}; islub S cl L; interval r a b ~= {} |] ==> L : interval r a b";
+Goal "[| a \\<in> A; b \\<in> A; S <= interval r a b; \
+\      S \\<noteq> {}; islub S cl L; interval r a b \\<noteq> {} |] ==> L \\<in> interval r a b";
 by (rtac intervalI 1);
 by (rtac a_less_lub 1);
 by (assume_tac 2);
@@ -594,7 +552,7 @@
 by (rtac ballI 1);
 by (afs [interval_lemma1] 1);
 by (afs [islubE1] 1);
-(* (L, b) : r *)
+(* (L, b) \\<in> r *)
 by (rtac islubE2 1);
 by (assume_tac 1);
 by (assume_tac 1);
@@ -602,8 +560,8 @@
 by (afs [interval_lemma2] 1);
 qed "L_in_interval";
 
-Goal "[| a : A; b : A; interval r a b ~= {}; S <= interval r a b; isglb S cl G; \
-\      S ~= {} |]   ==> G : interval r a b";
+Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {}; S <= interval r a b; isglb S cl G; \
+\      S \\<noteq> {} |]   ==> G \\<in> interval r a b";
 by (afs [interval_dual] 1);
 by (rtac (export L_in_interval) 1);
 by (rtac dualPO 1);
@@ -615,34 +573,34 @@
 by (assume_tac 1);
 qed "G_in_interval";
 
-Goal "[| a: A; b: A; interval r a b ~= {} |]\
-\  ==> (| pset = interval r a b, order = induced (interval r a b) r |) : PartialOrder";
+Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {} |]\
+\  ==> (| pset = interval r a b, order = induced (interval r a b) r |) \\<in> PartialOrder";
 by (rtac po_subset_po 1);
 by (afs [interval_subset] 1);
 qed "intervalPO";
 
-Goal "[| a : A; b : A;\
-\   interval r a b ~= {} |] ==> ! S. S <= interval r a b -->\
-\         (? L. islub S (| pset = interval r a b, order = induced (interval r a b) r |)  L)";
+Goal "[| a \\<in> A; b \\<in> A;\
+\   interval r a b \\<noteq> {} |] ==> \\<forall>S. S <= interval r a b -->\
+\         (\\<exists>L. islub S (| pset = interval r a b, order = induced (interval r a b) r |)  L)";
 by (strip_tac 1);
 by (forward_tac [S_intv_cl RS islubE] 1);
 by (assume_tac 2);
 by (assume_tac 1);
 by (etac exE 1);
-(* define the lub for the interval as: *)
+(* define the lub for the interval as *)
 by (res_inst_tac [("x","if S = {} then a else L")] exI 1);
 by (rtac (export islubI) 1);
-(* (if S = {} then a else L) : interval r a b *)
+(* (if S = {} then a else L) \\<in> interval r a b *)
 by (asm_full_simp_tac
     (simpset() addsimps [CompleteLatticeE1,L_in_interval]) 1);
 by (afs [left_in_interval] 1);
 (* lub prop 1 *)
 by (case_tac "S = {}" 1);
-(* S = {}, y: S = False => everything *)
+(* S = {}, y \\<in> S = False => everything *)
 by (Fast_tac 1);
-(* S ~= {} *)
+(* S \\<noteq> {} *)
 by (Asm_full_simp_tac 1);
-(* ! y:S. (y, L) : induced (interval r a b) r *)
+(* \\<forall>y:S. (y, L) \\<in> induced (interval r a b) r *)
 by (rtac ballI 1);
 by (afs [induced_def, L_in_interval] 1);
 by (rtac conjI 1);
@@ -650,8 +608,8 @@
 by (afs [S_intv_cl] 1);
 by (assume_tac 1);
 by (afs [islubE1] 1);
-(* ! z:interval r a b. (! y:S. (y, z) : induced (interval r a b) r -->
-      (if S = {} then a else L, z) : induced (interval r a b) r *)
+(* \\<forall>z:interval r a b. (\\<forall>y:S. (y, z) \\<in> induced (interval r a b) r -->
+      (if S = {} then a else L, z) \\<in> induced (interval r a b) r *)
 by (rtac ballI 1);
 by (rtac impI 1);
 by (case_tac "S = {}" 1);
@@ -665,7 +623,7 @@
 by (rtac interval_not_empty 1);
 by (rtac CompleteLatticeE13 1);
 by (afs [interval_def] 1);
-(* S ~= {} *)
+(* S \\<noteq> {} *)
 by (Asm_full_simp_tac 1);
 by (afs [induced_def, L_in_interval] 1);
 by (rtac islubE2 1);
@@ -678,7 +636,7 @@
 
 val intv_CL_glb = intv_CL_lub RS Rdual;
 
-Goal "[| a: A; b: A; interval r a b ~= {} |]\
+Goal "[| a \\<in> A; b \\<in> A; interval r a b \\<noteq> {} |]\
 \       ==> interval r a b <<= cl";
 by (rtac sublatticeI 1);
 by (afs [interval_subset] 1);
@@ -699,7 +657,7 @@
 by (afs [Top_def,Bot_def,least_def,greatest_def,dualA_iff, dualr_iff] 1);
 qed "Bot_dual_Top";
 
-Goal "Bot cl: A";
+Goal "Bot cl \\<in> A";
 by (simp_tac (simpset() addsimps [Bot_def,least_def]) 1);
 by (rtac someI2 1);
 by (fold_goals_tac [thm "A_def"]);
@@ -711,13 +669,13 @@
 by (afs [glbE1] 1);
 qed "Bot_in_lattice";
 
-Goal "Top cl: A";
+Goal "Top cl \\<in> A";
 by (simp_tac (simpset() addsimps [Top_dual_Bot, thm "A_def"]) 1);
 by (rtac (dualA_iff RS subst) 1);
 by (afs [export Bot_in_lattice,CL_dualCL] 1);
 qed "Top_in_lattice";
 
-Goal "x: A ==> (x, Top cl): r";
+Goal "x \\<in> A ==> (x, Top cl) \\<in> r";
 by (simp_tac (simpset() addsimps [Top_def,greatest_def]) 1);
 by (rtac someI2 1);
 by (fold_goals_tac [thm "r_def", thm "A_def"]);
@@ -728,7 +686,7 @@
 by (rtac subset_refl 1);
 qed "Top_prop";
 
-Goal "x: A ==> (Bot cl, x): r";
+Goal "x \\<in> A ==> (Bot cl, x) \\<in> r";
 by (simp_tac (simpset() addsimps [Bot_dual_Top, thm "r_def"]) 1);
 by (rtac (dualr_iff RS subst) 1);
 by (rtac (export Top_prop) 1);
@@ -736,14 +694,14 @@
 by (afs [dualA_iff, thm "A_def"] 1);
 qed "Bot_prop";
 
-Goal "x: A  ==> interval r x (Top cl) ~= {}";
+Goal "x \\<in> A  ==> interval r x (Top cl) \\<noteq> {}";
 by (rtac notI 1);
 by (dres_inst_tac [("a","Top cl")] equals0D 1);
 by (afs [interval_def] 1);
 by (afs [refl_def,Top_in_lattice,Top_prop] 1);
 qed "Top_intv_not_empty";
 
-Goal "x: A ==> interval r (Bot cl) x ~= {}";
+Goal "x \\<in> A ==> interval r (Bot cl) x \\<noteq> {}";
 by (simp_tac (simpset() addsimps [Bot_dual_Top]) 1);
 by (stac interval_dual 1);
 by (assume_tac 2);
@@ -755,7 +713,7 @@
 qed "Bot_intv_not_empty";
 
 (* fixed points form a partial order *)
-Goal "(| pset = P, order = induced P r|) : PartialOrder";
+Goal "(| pset = P, order = induced P r|) \\<in> PartialOrder";
 by (rtac po_subset_po 1);
 by (rtac fixfE1 1);
 qed "fixf_po";
@@ -767,11 +725,11 @@
 by (rtac (thm "Y_ss") 1);
 qed "Y_subset_A";
 
-Goal "lub Y cl : A";
+Goal "lub Y cl \\<in> A";
 by (afs [Y_subset_A RS lub_in_lattice] 1);
 qed "lubY_in_A";
 
-Goal "(lub Y cl, f (lub Y cl)): r";
+Goal "(lub Y cl, f (lub Y cl)) \\<in> r";
 by (rtac lubE2 1);
 by (rtac Y_subset_A 1);
 by (rtac (CLF_E1 RS funcset_mem) 1);
@@ -780,7 +738,7 @@
 by (rtac ballI 1);
 by (res_inst_tac [("t","x")] (fixfE2 RS subst) 1);
 by (etac (thm "Y_ss" RS subsetD) 1);
-(* reduce (f x, f (lub Y cl)) : r to (x, lub Y cl): r by monotonicity *)
+(* reduce (f x, f (lub Y cl)) \\<in> r to (x, lub Y cl) \\<in> r by monotonicity *)
 by (res_inst_tac [("f","f")] monotoneE 1);
 by (rtac CLF_E2 1);
 by (afs [Y_subset_A RS subsetD] 1);
@@ -796,40 +754,37 @@
 
 val intY1_elem = intY1_subset RS subsetD;
 
-Goal "(lam x: intY1. f x): intY1 funcset intY1";
-by (rtac restrictI 1);
+Goal "x \\<in> intY1 \\<Longrightarrow> f x \\<in> intY1";
 by (afs [thm "intY1_def", interval_def] 1);
 by (rtac conjI 1);
 by (rtac transE 1);
 by (rtac CompleteLatticeE13 1);
 by (rtac lubY_le_flubY 1);
-(* (f (lub Y cl), f x) : r *)
+(* (f (lub Y cl), f x) \\<in> r *)
 by (res_inst_tac [("f","f")]monotoneE 1);
 by (rtac CLF_E2 1);
 by (rtac lubY_in_A 1);
 by (afs [thm "intY1_def",interval_def, intY1_elem] 1);
 by (afs [thm "intY1_def", interval_def] 1);
-(* (f x, Top cl) : r *)
+(* (f x, Top cl) \\<in> r *)
 by (rtac Top_prop 1);
 by (rtac (CLF_E1 RS funcset_mem) 1);
 by (afs [thm "intY1_def",interval_def, intY1_elem] 1);
+qed "intY1_f_closed";
+
+Goal "(lam x: intY1. f x) \\<in> intY1 funcset intY1";
+by (rtac restrictI 1);
+by (etac intY1_f_closed 1); 
 qed "intY1_func";
 
 Goal "monotone (lam x: intY1. f x) intY1 (induced intY1 r)";
-by (simp_tac (simpset() addsimps [monotone_def]) 1);
-by (Clarify_tac 1);
-by (simp_tac (simpset() addsimps [induced_def]) 1);
-by (afs [intY1_func RS funcset_mem] 1);
-by (afs [restrict_apply1] 1);
-by (res_inst_tac [("f","f")] monotoneE 1);
-by (rtac CLF_E2 1);
-by (etac (intY1_subset RS subsetD) 2);
-by (etac (intY1_subset RS subsetD) 1);
-by (afs [induced_def] 1);
+by (auto_tac (claset(), 
+            simpset() addsimps [monotone_def, induced_def, intY1_f_closed])); 
+by (blast_tac (claset() addIs [intY1_elem, CLF_E2 RS monotoneE]) 1); 
 qed "intY1_mono";
 
 Goalw [thm "intY1_def"]
-    "(| pset = intY1, order = induced intY1 r |): CompleteLattice";
+    "(| pset = intY1, order = induced intY1 r |) \\<in> CompleteLattice";
 by (rtac interv_is_compl_latt 1);
 by (rtac lubY_in_A 1);
 by (rtac Top_in_lattice 1);
@@ -837,7 +792,7 @@
 by (rtac lubY_in_A 1);
 qed "intY1_is_cl";
 
-Goalw  [thm "P_def"] "v : P";
+Goalw  [thm "P_def"] "v \\<in> P";
 by (res_inst_tac [("A","intY1")] fixf_subset 1);
 by (rtac intY1_subset 1);
 by (rewrite_goals_tac [thm "v_def"]);
@@ -847,7 +802,7 @@
 qed "v_in_P";
 
 Goalw [thm "intY1_def"]
-     "[| z : P; ! y:Y. (y, z) : induced P r |] ==> z : intY1";
+     "[| z \\<in> P; \\<forall>y\\<in>Y. (y, z) \\<in> induced P r |] ==> z \\<in> intY1";
 by (rtac intervalI 1);
 by (etac (fixfE1 RS subsetD RS Top_prop) 2);
 by (rtac lubE2 1);
@@ -859,26 +814,20 @@
 by (afs [induced_def] 1);
 qed "z_in_interval";
 
-Goal "[| z : P; ! y:Y. (y, z) : induced P r |]\
-\     ==> ((lam x: intY1. f x) z, z) : induced intY1 r";
-by (afs [induced_def,intY1_func RS funcset_mem, z_in_interval] 1);
-by (rtac (z_in_interval RS restrict_apply1 RS ssubst) 1);
-by (assume_tac 1);
-by (afs [induced_def] 1);
-by (afs [fixfE2] 1);
-by (rtac reflE 1);
-by (rtac CompleteLatticeE11 1);
-by (etac (fixfE1 RS subsetD) 1);
+Goal "[| z \\<in> P; \\<forall>y\\<in>Y. (y, z) \\<in> induced P r |]\
+\     ==> ((lam x: intY1. f x) z, z) \\<in> induced intY1 r";
+by (afs [induced_def, intY1_f_closed, z_in_interval] 1);
+by (afs [fixfE2, fixfE1 RS subsetD, CompleteLatticeE11 RS reflE] 1);
 qed "f'z_in_int_rel";
 
-Goal "? L. islub Y (| pset = P, order = induced P r |) L";
+Goal "\\<exists>L. islub Y (| pset = P, order = induced P r |) L";
 by (res_inst_tac [("x","v")] exI 1);
 by (simp_tac (simpset() addsimps [islub_def]) 1);
-(* v : P *)
+(* v \\<in> P *)
 by (afs [v_in_P] 1);
 by (rtac conjI 1);
 (* v is lub *)
-(*  1. ! y:Y. (y, v) : induced P r *)
+(*  1. \\<forall>y:Y. (y, v) \\<in> induced P r *)
 by (rtac ballI 1);
 by (afs [induced_def, subsetD, v_in_P] 1);
 by (rtac conjI 1);
@@ -892,10 +841,7 @@
 by (afs [thm "v_def"] 1);
 by (fold_goals_tac [thm "intY1_def"]);
 by (rtac (simplify (simpset()) (intY1_is_cl RS export glb_in_lattice)) 1);
-by (Simp_tac 1);
-by (rtac subsetI 1);
-by (dtac CollectD 1);
-by (etac conjunct2 1);
+by (Force_tac 1); 
 (* v is LEAST ub *)
 by (Clarify_tac 1);
 by (rtac indI 1);
@@ -905,17 +851,15 @@
 by (rtac indE 1);
 by (rtac intY1_subset 2);
 by (rtac (simplify (simpset()) (intY1_is_cl RS export (glbE1 RS bspec))) 1);
-by (Simp_tac 1);
-by (rtac subsetI 1);
-by (dtac CollectD 1);
-by (etac conjunct2 1);
-by (afs [f'z_in_int_rel, z_in_interval] 1);
+by (Force_tac 1); 
+by (afs [induced_def, intY1_f_closed, z_in_interval] 1);
+by (afs [fixfE2, fixfE1 RS subsetD, CompleteLatticeE11 RS reflE] 1);
 qed "tarski_full_lemma";
 val Tarski_full_lemma = Export tarski_full_lemma;
 
 Close_locale "Tarski";
 
-Goal "(| pset = P, order = induced P r|) : CompleteLattice";
+Goal "(| pset = P, order = induced P r|) \\<in> CompleteLattice";
 by (rtac CompleteLatticeI_simp 1);
 by (afs [fixf_po] 1);
 by (Clarify_tac 1);