--- a/src/HOL/ex/MT.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/ex/MT.ML Mon Nov 03 12:13:18 1997 +0100
@@ -24,7 +24,7 @@
val infsys_mono_tac = (REPEAT (ares_tac (basic_monos@[allI,impI]) 1));
val prems = goal MT.thy "P a b ==> P (fst (a,b)) (snd (a,b))";
-by (simp_tac (!simpset addsimps prems) 1);
+by (simp_tac (simpset() addsimps prems) 1);
qed "infsys_p1";
val prems = goal MT.thy "!!a b. P (fst (a,b)) (snd (a,b)) ==> P a b";
@@ -83,7 +83,7 @@
by (rtac (monoh RS monoD) 1);
by (rtac (UnE RS subsetI) 1);
by (assume_tac 1);
-by (blast_tac (!claset addSIs [cih]) 1);
+by (blast_tac (claset() addSIs [cih]) 1);
by (rtac (monoh RS monoD RS subsetD) 1);
by (rtac Un_upper2 1);
by (etac (monoh RS gfp_lemma2 RS subsetD) 1);
@@ -151,7 +151,7 @@
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
(*Naughty! But the quantifiers are nested VERY deeply...*)
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_const";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -160,7 +160,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_var2";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -169,7 +169,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_fn";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -179,7 +179,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_fix";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -189,7 +189,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "eval_app1";
val prems = goalw MT.thy [eval_def, eval_rel_def]
@@ -202,7 +202,7 @@
by (rtac lfp_intro2 1);
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
-by (blast_tac (!claset addSIs [disjI2]) 1);
+by (blast_tac (claset() addSIs [disjI2]) 1);
qed "eval_app2";
(* Strong elimination, induction on evaluations *)
@@ -230,7 +230,7 @@
by (rtac eval_fun_mono 1);
by (rewtac eval_fun_def);
by (dtac CollectD 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (ALLGOALS (resolve_tac prems));
by (ALLGOALS (Blast_tac));
qed "eval_ind0";
@@ -274,7 +274,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "elab_const";
goalw MT.thy [elab_def, elab_rel_def]
@@ -282,7 +282,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "elab_var";
goalw MT.thy [elab_def, elab_rel_def]
@@ -290,7 +290,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "elab_fn";
goalw MT.thy [elab_def, elab_rel_def]
@@ -299,7 +299,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (blast_tac (!claset addSIs [exI]) 1);
+by (blast_tac (claset() addSIs [exI]) 1);
qed "elab_fix";
goalw MT.thy [elab_def, elab_rel_def]
@@ -308,7 +308,7 @@
by (rtac lfp_intro2 1);
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
-by (blast_tac (!claset addSIs [disjI2]) 1);
+by (blast_tac (claset() addSIs [disjI2]) 1);
qed "elab_app";
(* Strong elimination, induction on elaborations *)
@@ -336,7 +336,7 @@
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
by (dtac CollectD 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (ALLGOALS (resolve_tac prems));
by (ALLGOALS (Blast_tac));
qed "elab_ind0";
@@ -387,7 +387,7 @@
by (rtac elab_fun_mono 1);
by (rewtac elab_fun_def);
by (dtac CollectD 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (ALLGOALS (resolve_tac prems));
by (ALLGOALS (Blast_tac));
qed "elab_elim0";
@@ -552,7 +552,7 @@
by (rewtac hasty_fun_def);
by (dtac CollectD 1);
by (fold_goals_tac [hasty_fun_def]);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (REPEAT (ares_tac prems 1));
qed "hasty_rel_elim0";
@@ -581,7 +581,7 @@
goalw MT.thy [hasty_def,hasty_env_def]
"!!t. te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t";
by (rtac hasty_rel_clos_coind 1);
-by (ALLGOALS (blast_tac (!claset delrules [equalityI])));
+by (ALLGOALS (blast_tac (claset() delrules [equalityI])));
qed "hasty_clos";
(* Elimination on constants for hasty *)
@@ -623,13 +623,13 @@
"!!ve. [| ve hastyenv te; v hasty t |] ==> \
\ ve + {ev |-> v} hastyenv te + {ev |=> t}";
by (rewtac hasty_env_def);
-by (asm_full_simp_tac (!simpset delsimps mem_simps
+by (asm_full_simp_tac (simpset() delsimps mem_simps
addsimps [ve_dom_owr, te_dom_owr]) 1);
by (safe_tac HOL_cs);
by (excluded_middle_tac "ev=x" 1);
-by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
by (Blast_tac 1);
-by (asm_simp_tac (!simpset addsimps [ve_app_owr1, te_app_owr1]) 1);
+by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1);
qed "hasty_env1";
(* ############################################################ *)
@@ -668,15 +668,15 @@
by ((forward_tac [ssubst] 1) THEN (assume_tac 2));
by (rtac hasty_rel_clos_coind 1);
by (etac elab_fn 1);
-by (asm_simp_tac (!simpset addsimps [ve_dom_owr, te_dom_owr]) 1);
+by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1);
-by (asm_simp_tac (!simpset delsimps mem_simps addsimps [ve_dom_owr]) 1);
+by (asm_simp_tac (simpset() delsimps mem_simps addsimps [ve_dom_owr]) 1);
by (safe_tac HOL_cs);
by (excluded_middle_tac "ev2=ev1a" 1);
-by (asm_full_simp_tac (!simpset addsimps [ve_app_owr2, te_app_owr2]) 1);
+by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
by (Blast_tac 1);
-by (asm_simp_tac (!simpset delsimps mem_simps
+by (asm_simp_tac (simpset() delsimps mem_simps
addsimps [ve_app_owr1, te_app_owr1]) 1);
by (hyp_subst_tac 1);
by (etac subst 1);
@@ -690,7 +690,7 @@
\ |] ==> \
\ v_const(c_app c1 c2) hasty t";
by (dtac elab_app_elim 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (rtac hasty_const 1);
by (rtac isof_app 1);
by (rtac hasty_elim_const 1);
@@ -711,7 +711,7 @@
\ |] ==> \
\ v hasty t";
by (dtac elab_app_elim 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
by (assume_tac 1);
by (etac impE 1);
@@ -721,9 +721,9 @@
by (etac impE 1);
by (assume_tac 1);
by (dtac hasty_elim_clos 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (dtac elab_fn_elim 1);
-by (blast_tac (!claset addIs [hasty_env1] addSDs [t_fun_inj]) 1);
+by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
qed "consistency_app2";
val [major] = goal MT.thy
@@ -733,7 +733,7 @@
(* Proof by induction on the structure of evaluations *)
by (rtac (major RS eval_ind) 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (DEPTH_SOLVE
(ares_tac [consistency_const, consistency_var, consistency_fn,
consistency_fix, consistency_app1, consistency_app2] 1));
@@ -746,7 +746,7 @@
val prems = goalw MT.thy [isof_env_def,hasty_env_def]
"ve isofenv te ==> ve hastyenv te";
by (cut_facts_tac prems 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (etac allE 1);
by (etac impE 1);
by (assume_tac 1);
@@ -761,7 +761,7 @@
by (cut_facts_tac prems 1);
by (rtac hasty_elim_const 1);
by (dtac consistency 1);
-by (blast_tac (!claset addSIs [basic_consistency_lem]) 1);
+by (blast_tac (claset() addSIs [basic_consistency_lem]) 1);
qed "basic_consistency";
writeln"Reached end of file.";