--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Nov 03 14:06:27 1997 +0100
@@ -13,15 +13,15 @@
(* ---------------------------------------------------------------------------- *)
goal thy "laststate (s,UU) = s";
-by (simp_tac (!simpset addsimps [laststate_def]) 1);
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
qed"laststate_UU";
goal thy "laststate (s,nil) = s";
-by (simp_tac (!simpset addsimps [laststate_def]) 1);
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
qed"laststate_nil";
goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
-by (simp_tac (!simpset addsimps [laststate_def]) 1);
+by (simp_tac (simpset() addsimps [laststate_def]) 1);
by (case_tac "ex=nil" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
@@ -45,14 +45,14 @@
goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
by (res_inst_tac [("x","(a,t)>>nil")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"transition_is_ex";
goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
by (res_inst_tac [("x","nil")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"nothing_is_ex";
@@ -60,7 +60,7 @@
\ ==> ? ex. move A ex s a s''";
by (res_inst_tac [("x","(a,s')>>(a',s'')>>nil")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"ei_transitions_are_ex";
@@ -70,7 +70,7 @@
\ ? ex. move A ex s1 a1 s4";
by (res_inst_tac [("x","(a1,s2)>>(a2,s3)>>(a3,s4)>>nil")] exI 1);
-by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [move_def]) 1);
qed"eii_transitions_are_ex";
@@ -92,23 +92,23 @@
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (!claset addDs prems) 1);
+ by(fast_tac (claset() addDs prems) 1);
val lemma = result();
goal thy "!!f.[| is_weak_ref_map f C A |]\
\ ==> (is_weak_ref_map f (rename C g) (rename A g))";
-by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
by (rtac conjI 1);
(* 1: start states *)
-by (asm_full_simp_tac (!simpset addsimps [rename_def,rename_set_def,starts_of_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [rename_def,rename_set_def,starts_of_def]) 1);
(* 2: reachable transitions *)
by (REPEAT (rtac allI 1));
by (rtac lemma 1);
-by (simp_tac (!simpset addsimps [rename_def,rename_set_def]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
+by (simp_tac (simpset() addsimps [rename_def,rename_set_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,
asig_outputs_def,asig_of_def,trans_of_def]) 1);
-by (safe_tac (!claset));
+by (safe_tac (claset()));
by (stac expand_if 1);
by (rtac conjI 1);
by (rtac impI 1);
@@ -132,7 +132,7 @@
by (forward_tac [reachable_rename] 1);
by (Asm_full_simp_tac 1);
(* x is internal *)
-by (simp_tac (!simpset addcongs [conj_cong]) 1);
+by (simp_tac (simpset() addcongs [conj_cong]) 1);
by (rtac impI 1);
by (etac conjE 1);
by (forward_tac [reachable_rename] 1);