src/HOL/ex/PiSets.ML

--- a/src/HOL/ex/PiSets.ML	Mon Sep 21 23:06:37 1998 +0200
+++ b/src/HOL/ex/PiSets.ML	Mon Sep 21 23:12:31 1998 +0200
@@ -613,9 +613,7 @@
 \                ==> f x = g x";
 by (etac equalityE 1);
 by (rewtac subset_def);
-by (dres_inst_tac [("x","(x, f x)")] bspec 1);
-by (Fast_tac 1);
-by (Fast_tac 1);
+by (Auto_tac);
 val set_eq_lemma = result();
 
 goal PiSets.thy "!! A B. inj_on (PiBij A B) (Pi A B)";
@@ -639,64 +637,59 @@
 
 goal PiSets.thy "!!A B. PiBij A B `` (Pi A B) = Graph A B";
 by (rtac equalityI 1);
-by (afs [image_def] 1);
-by (rtac subsetI 1);
-by (Asm_full_simp_tac 1);
-by (etac bexE 1);
-by (etac ssubst 1);
-by (afs [PiBij_in_Graph] 1);
+by (force_tac (claset(), simpset() addsimps [image_def,PiBij_in_Graph]) 1);
 by (rtac subsetI 1);
 by (afs [image_def] 1);
 by (res_inst_tac [("x","lam a: A. @ y. (a, y): x")] bexI 1);
-by (rtac restrictI_Pi 2);
-by (strip 2);
-by (rtac ex1E 2);
-by (afs [Graph_def] 2);
-by (etac conjE 2);
-by (dtac bspec 2);
-by (assume_tac 2);
-by (assume_tac 2);
-by (stac select_equality 2);
-by (assume_tac 2);
-by (Blast_tac 2);
+ by (rtac restrictI_Pi 2);
+ by (strip 2);
+ by (rtac ex1E 2);
+  by (afs [Graph_def] 2);
+  by (etac conjE 2);
+  by (dtac bspec 2);
+   by (assume_tac 2);
+  by (assume_tac 2);
+ by (stac select_equality 2);
+   by (assume_tac 2);
+  by (Blast_tac 2);
 (* gets hung up on by (afs [Graph_def] 2); *)
-by (SELECT_GOAL (rewtac Graph_def) 2);
-by (Blast_tac 2);
+ by (SELECT_GOAL (rewtac Graph_def) 2);
+ by (Blast_tac 2);
 (* x = PiBij A B (lam a:A. @ y. (a, y) : x) *)
 by (afs [PiBij_def,Graph_def] 1);
 by (stac restrictE1 1);
-by (rtac restrictI_Pi 1);
+ by (rtac restrictI_Pi 1);
 (* again like the old 2. subgoal *)
-by (strip 1);
-by (rtac ex1E 1);
-by (etac conjE 1);
-by (dtac bspec 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (stac select_equality 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
+ by (strip 1);
+ by (rtac ex1E 1);
+  by (etac conjE 1);
+  by (dtac bspec 1);
+   by (assume_tac 1);
+  by (assume_tac 1);
+ by (stac select_equality 1);
+   by (assume_tac 1);
+  by (Blast_tac 1);
+ by (Blast_tac 1);
 (* *)
 by (rtac equalityI 1);
 by (rtac subsetI 1);
-by (rtac CollectI 1);
-by (split_all_tac 1);
-by (Simp_tac 1);
-by (rtac conjI 1);
-by (Blast_tac 1);
-by (etac conjE 1);
-by (dtac subsetD 1);
-by (assume_tac 1);
-by (dtac SigmaD1 1);
-by (dtac bspec 1);
-by (assume_tac 1);
-by (stac restrictE1 1);
-by (assume_tac 1);
-by (rtac sym 1);
-by (rtac select_equality 1);
-by (assume_tac 1);
-by (Blast_tac 1);
+ by (rtac CollectI 1);
+ by (split_all_tac 1);
+ by (Simp_tac 1);
+ by (rtac conjI 1);
+  by (Blast_tac 1);
+ by (etac conjE 1);
+ by (dtac subsetD 1);
+  by (assume_tac 1);
+ by (dtac SigmaD1 1);
+ by (dtac bspec 1);
+  by (assume_tac 1);
+ by (stac restrictE1 1);
+  by (assume_tac 1);
+ by (rtac sym 1);
+ by (rtac select_equality 1);
+  by (assume_tac 1);
+ by (Blast_tac 1);
 (* {(xa,y). xa : A & y = (lam a:A. @ y. (a, y) : x) xa} <= x   *)
 by (rtac subsetI 1);
 by (Asm_full_simp_tac 1);
@@ -706,7 +699,7 @@
 by (etac conjE 1);
 by (afs [restrictE1] 1);
 by (dtac bspec 1);
-by (assume_tac 1);
+ by (assume_tac 1);
 by (dtac Ex1_Ex 1);
 by (rewtac Ex_def);
 by (assume_tac 1);