--- a/src/HOLCF/IOA/Storage/Correctness.ML Thu Jan 28 18:28:06 1999 +0100
+++ b/src/HOLCF/IOA/Storage/Correctness.ML Fri Jan 29 16:23:56 1999 +0100
@@ -28,7 +28,7 @@
(* ---------------- main-part ------------------- *)
by (REPEAT (rtac allI 1));
-br imp_conj_lemma 1;
+by (rtac imp_conj_lemma 1);
ren "k b used c k' b' a" 1;
by (induct_tac "a" 1);
by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
@@ -37,13 +37,13 @@
(* NEW *)
by (res_inst_tac [("x","(used,True)")] exI 1);
by (Asm_full_simp_tac 1);
-br transition_is_ex 1;
+by (rtac transition_is_ex 1);
by (simp_tac (simpset() addsimps [
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
(* LOC *)
by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
by (Asm_full_simp_tac 1);
-br transition_is_ex 1;
+by (rtac transition_is_ex 1);
by (simp_tac (simpset() addsimps [
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
by (Fast_tac 1);
@@ -51,8 +51,8 @@
by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
by (Asm_full_simp_tac 1);
by (SELECT_GOAL (safe_tac set_cs) 1);
-auto();
-br transition_is_ex 1;
+by Auto_tac;
+by (rtac transition_is_ex 1);
by (simp_tac (simpset() addsimps [
Spec.ioa_def,Spec.trans_def,trans_of_def])1);
qed"issimulation";
@@ -61,14 +61,14 @@
Goalw [ioa_implements_def]
"impl_ioa =<| spec_ioa";
-br conjI 1;
+by (rtac conjI 1);
by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
Impl.ioa_def,Spec.ioa_def, asig_outputs_def,asig_of_def,
asig_inputs_def]) 1);
-br trace_inclusion_for_simulations 1;
+by (rtac trace_inclusion_for_simulations 1);
by (simp_tac (simpset() addsimps [Impl.sig_def,Spec.sig_def,
Impl.ioa_def,Spec.ioa_def, externals_def,asig_outputs_def,asig_of_def,
asig_inputs_def]) 1);
-br issimulation 1;
+by (rtac issimulation 1);
qed"implementation";