--- a/src/HOLCF/IOA/NTP/Correctness.ML Mon Nov 03 12:36:48 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Mon Nov 03 14:06:27 1997 +0100
@@ -15,11 +15,11 @@
val impl_asigs = [Sender.sender_asig_def,Receiver.receiver_asig_def,
Abschannel.srch_asig_def,Abschannel.rsch_asig_def];
-(* Two simpsets: - !simpset is basic, ss' unfolds hom_ioas *)
+(* Two simpsets: - simpset() is basic, ss' unfolds hom_ioas *)
Delsimps [split_paired_All];
-val ss' = (!simpset addsimps hom_ioas);
+val ss' = (simpset() addsimps hom_ioas);
(* A lemma about restricting the action signature of the implementation
@@ -38,22 +38,22 @@
\ | C_m_r => False \
\ | C_r_s => False \
\ | C_r_r(m) => False)";
- by (simp_tac (!simpset addsimps ([externals_def, restrict_def,
+ by (simp_tac (simpset() addsimps ([externals_def, restrict_def,
restrict_asig_def, Spec.sig_def]
@asig_projections)) 1);
by (Action.action.induct_tac "a" 1);
- by (ALLGOALS(simp_tac (!simpset addsimps [actions_def]@asig_projections)));
+ by (ALLGOALS(simp_tac (simpset() addsimps [actions_def]@asig_projections)));
(* 2 *)
- by (simp_tac (!simpset addsimps impl_ioas) 1);
- by (simp_tac (!simpset addsimps impl_asigs) 1);
- by (simp_tac (!simpset addsimps
+ by (simp_tac (simpset() addsimps impl_ioas) 1);
+ by (simp_tac (simpset() addsimps impl_asigs) 1);
+ by (simp_tac (simpset() addsimps
[asig_of_par, asig_comp_def]@asig_projections) 1);
by (simp_tac rename_ss 1);
(* 1 *)
- by (simp_tac (!simpset addsimps impl_ioas) 1);
- by (simp_tac (!simpset addsimps impl_asigs) 1);
- by (simp_tac (!simpset addsimps
+ by (simp_tac (simpset() addsimps impl_ioas) 1);
+ by (simp_tac (simpset() addsimps impl_asigs) 1);
+ by (simp_tac (simpset() addsimps
[asig_of_par, asig_comp_def]@asig_projections) 1);
qed "externals_lemma";
@@ -66,18 +66,18 @@
(* Proof of correctness *)
goalw Correctness.thy [Spec.ioa_def, is_weak_ref_map_def]
"is_weak_ref_map hom (restrict impl_ioa (externals spec_sig)) spec_ioa";
-by (simp_tac (!simpset addsimps
+by (simp_tac (simpset() addsimps
[Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
by (rtac conjI 1);
by (simp_tac ss' 1);
-by (asm_simp_tac (!simpset addsimps sels) 1);
+by (asm_simp_tac (simpset() addsimps sels) 1);
by (REPEAT(rtac allI 1));
by (rtac imp_conj_lemma 1); (* from lemmas.ML *)
by (Action.action.induct_tac "a" 1);
by (asm_simp_tac (ss' setloop (split_tac [expand_if])) 1);
by (forward_tac [inv4] 1);
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
by (simp_tac ss' 1);
@@ -91,7 +91,7 @@
by (forward_tac [inv2] 1);
by (etac disjE 1);
by (Asm_simp_tac 1);
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (asm_simp_tac ss' 1);
by (forward_tac [inv2] 1);
@@ -101,14 +101,14 @@
by (case_tac "sq(sen(s))=[]" 1);
by (asm_full_simp_tac ss' 1);
-by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
by (case_tac "m = hd(sq(sen(s)))" 1);
-by (fast_tac (!claset addss (!simpset addsimps [neq_Nil_conv])) 1);
+by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
by (Asm_full_simp_tac 1);
-by (fast_tac (!claset addSDs [add_leD1 RS leD]) 1);
+by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
by (Asm_full_simp_tac 1);
qed"ntp_correct";