--- a/src/ZF/Coind/Map.ML Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/Coind/Map.ML Fri Jan 03 15:01:55 1997 +0100
@@ -38,7 +38,7 @@
by (rtac ([Sigma_mono, product_univ] MRS subset_trans) 1);
by (etac subset_trans 1);
by (rtac (arg_subset_eclose RS univ_mono) 1);
-by (simp_tac (ZF_ss addsimps [Union_Pow_eq]) 1);
+by (simp_tac (!simpset addsimps [Union_Pow_eq]) 1);
qed "MapQU_lemma";
(* Theorems *)
@@ -49,7 +49,7 @@
by (rtac (MapQU_lemma RS subsetD) 1);
by (rtac subsetI 1);
by (eresolve_tac prems 1);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "mapQU";
(* ############################################################ *)
@@ -57,7 +57,7 @@
(* ############################################################ *)
goalw Map.thy [PMap_def,TMap_def] "!!A.B<=C ==> PMap(A,B)<=PMap(A,C)";
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "map_mono";
(* Rename to pmap_mono *)
@@ -69,7 +69,7 @@
(** map_emp **)
goalw Map.thy [map_emp_def,PMap_def,TMap_def] "map_emp:PMap(A,B)";
-by (safe_tac ZF_cs);
+by (safe_tac (!claset));
by (rtac image_02 1);
qed "pmap_empI";
@@ -78,21 +78,21 @@
goalw Map.thy [map_owr_def,PMap_def,TMap_def]
"!! A.[| m:PMap(A,B); a:A; b:B |] ==> map_owr(m,a,b):PMap(A,B)";
-by (safe_tac ZF_cs);
-by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [if_iff])));
-by (fast_tac ZF_cs 1);
-by (fast_tac ZF_cs 1);
-by (fast_tac ZF_cs 1);
-
+by (Step_tac 1);
+by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [if_iff])));
+by (Fast_tac 1);
+by (Fast_tac 1);
+by (Deepen_tac 2 1);
+(*Remaining subgoal*)
by (rtac (excluded_middle RS disjE) 1);
by (etac image_Sigma1 1);
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 1);
by (asm_full_simp_tac
- (ZF_ss addsimps [qbeta] setloop split_tac [expand_if]) 1);
-by (safe_tac FOL_cs);
+ (!simpset addsimps [qbeta] setloop split_tac [expand_if]) 1);
+by (safe_tac (!claset));
by (dres_inst_tac [("psi", "?uu ~: B")] asm_rl 3);
-by (ALLGOALS (asm_full_simp_tac ZF_ss));
-by (fast_tac ZF_cs 1);
+by (ALLGOALS Asm_full_simp_tac);
+by (Fast_tac 1);
qed "pmap_owrI";
(** map_app **)
@@ -101,7 +101,7 @@
"!!m.[| m:TMap(A,B); a:domain(m) |] ==> map_app(m,a) ~=0";
by (etac domainE 1);
by (dtac imageI 1);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
by (etac not_emptyI 1);
qed "tmap_app_notempty";
@@ -116,7 +116,7 @@
by (assume_tac 1);
by (dtac tmap_appI 1);
by (assume_tac 1);
-by (fast_tac ZF_cs 1);
+by (Fast_tac 1);
qed "pmap_appI";
(** domain **)
@@ -144,7 +144,7 @@
qed "domain_UN";
goal Map.thy "domain(Sigma(A,B)) = {x:A.EX y.y:B(x)}";
-by (simp_tac (ZF_ss addsimps [domain_UN,domain_0,domain_cons]) 1);
+by (simp_tac (!simpset addsimps [domain_UN,domain_0,domain_cons]) 1);
by (fast_tac eq_cs 1);
qed "domain_Sigma";
@@ -156,7 +156,7 @@
goalw Map.thy [map_owr_def]
"!!a.b ~= 0 ==> domain(map_owr(f,a,b)) = {a} Un domain(f)";
-by (simp_tac (if_ss addsimps [domain_Sigma]) 1);
+by (simp_tac (!simpset addsimps [domain_Sigma]) 1);
by (rtac equalityI 1);
by (fast_tac eq_cs 1);
by (rtac subsetI 1);
@@ -164,11 +164,9 @@
by (assume_tac 1);
by (etac UnE' 1);
by (etac singletonE 1);
-by (asm_simp_tac if_ss 1);
+by (Asm_simp_tac 1);
by (fast_tac eq_cs 1);
-by (etac notsingletonE 1);
-by (asm_simp_tac if_ss 1);
-by (fast_tac eq_cs 1);
+by (fast_tac (eq_cs addss (!simpset)) 1);
qed "map_domain_owr";
(** Application **)
@@ -176,8 +174,8 @@
goalw Map.thy [map_app_def,map_owr_def]
"map_app(map_owr(f,a,b),a) = b";
by (stac qbeta 1);
-by (fast_tac ZF_cs 1);
-by (simp_tac if_ss 1);
+by (Fast_tac 1);
+by (Simp_tac 1);
qed "map_app_owr1";
goalw Map.thy [map_app_def,map_owr_def]
@@ -187,7 +185,7 @@
by (assume_tac 1);
by (fast_tac eq_cs 1);
by (etac (qbeta RS ssubst) 1);
-by (asm_simp_tac if_ss 1);
+by (Asm_simp_tac 1);
qed "map_app_owr2";