--- a/src/HOL/UNITY/Handshake.ML Wed Dec 02 16:14:09 1998 +0100
+++ b/src/HOL/UNITY/Handshake.ML Thu Dec 03 10:45:06 1998 +0100
@@ -11,6 +11,7 @@
(*split_all_tac causes a big blow-up*)
claset_ref() := claset() delSWrapper record_split_name;
+Addsimps [F_def RS def_prg_States, G_def RS def_prg_States];
Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
program_defs_ref := [F_def, G_def];
@@ -20,7 +21,6 @@
Addsimps (thms"state.update_defs");
Addsimps [simp_of_set invFG_def];
-
Goal "(F Join G) : Invariant invFG";
by (rtac InvariantI 1);
by (Force_tac 1);
@@ -36,12 +36,14 @@
by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (ensures_tac "cmdG" 2);
by (constrains_tac 1);
+by Auto_tac;
qed "lemma2_1";
Goal "(F Join G) : LeadsTo ({s. NF s = k} Int {s. BB s}) {s. k < NF s}";
by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (constrains_tac 2);
by (ensures_tac "cmdF" 1);
+by Auto_tac;
qed "lemma2_2";