--- a/src/HOL/UNITY/Client.ML Mon Mar 01 18:37:52 1999 +0100
+++ b/src/HOL/UNITY/Client.ML Mon Mar 01 18:38:43 1999 +0100
@@ -90,8 +90,7 @@
(*** Towards proving the liveness property ***)
-Goal "States Cli_prg = States G \
-\ ==> Cli_prg Join G \
+Goal "Cli_prg Join G \
\ : transient {s. size (giv s) = Suc k & \
\ size (rel s) = k & ask s ! k <= giv s ! k}";
by (res_inst_tac [("act", "rel_act")] transient_mem 1);
@@ -131,13 +130,11 @@
by (Clarify_tac 1);
by (rtac Stable_transient_reachable_LeadsTo 1);
by (res_inst_tac [("k", "k")] transient_lemma 2);
-by (etac Disjoint_States_eq 2);
by (force_tac (claset() addDs [impOfSubs Increasing_size,
impOfSubs Increasing_Stable_less],
simpset()) 1);
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
by (Blast_tac 1);
-by (etac Disjoint_States_eq 1);
by (auto_tac (claset(),
simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
by (ALLGOALS Force_tac);