# HG changeset patch
# User paulson
# Date 908268933 -7200
# Node ID 29d8e53a4920e3380cb5750986135d8c73591874
# Parent  2570d7c3f6e7e74ad2e490b924d26ec8e8cdf986
tidied

diff -r 2570d7c3f6e7 -r 29d8e53a4920 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Tue Oct 13 10:50:56 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Tue Oct 13 10:55:33 1998 +0200
@@ -92,7 +92,7 @@
 by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
 qed "LeadsTo_Un";
 
-Goal "[| A <= B |] ==> LeadsTo F A B";
+Goal "A <= B ==> LeadsTo F A B";
 by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
 by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
 qed "subset_imp_LeadsTo";
@@ -178,11 +178,8 @@
 \        LeadsTo F A A';   \
 \        INV Int B  <= A;  INV Int A' <= B' |] \
 \     ==> LeadsTo F B B'";
-by (rtac Invariant_LeadsToI 1);
-by (assume_tac 1);
-by (dtac Invariant_LeadsToD 1);
-by (assume_tac 1);
-by (blast_tac (claset()addIs [LeadsTo_weaken]) 1);
+by (REPEAT (ares_tac [Invariant_includes_reachable, 
+		      reachable_LeadsTo_weaken] 1));
 qed "Invariant_LeadsTo_weaken";
 
 
@@ -269,9 +266,8 @@
 
 (** PSP: Progress-Safety-Progress **)
 
-(*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
-Goal
-  "[| LeadsTo F A A';  Stable F B |] ==> LeadsTo F (A Int B) (A' Int B)";
+(*Special case of PSP: Misra's "stable conjunction"*)
+Goal "[| LeadsTo F A A';  Stable F B |] ==> LeadsTo F (A Int B) (A' Int B)";
 by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
 by (dtac psp_stable 1);
 by (assume_tac 1);
diff -r 2570d7c3f6e7 -r 29d8e53a4920 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Tue Oct 13 10:50:56 1998 +0200
+++ b/src/HOL/UNITY/Union.ML	Tue Oct 13 10:55:33 1998 +0200
@@ -163,7 +163,7 @@
 qed "ensures_Join";
 
 Goalw [stable_def, constrains_def, Join_def]
-    "[| stable (Acts F) A;  constrains (Acts G) A A';  Id: Acts G |] \
+    "[| stable (Acts F) A;  constrains (Acts G) A A' |] \
 \    ==> constrains (Acts (F Join G)) A A'";
 by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
 by (Blast_tac 1);
@@ -172,7 +172,7 @@
 (*Premises cannot use Invariant because  Stable F A  is weaker than
   stable (Acts G) A *)
 Goal "[| stable (Acts F) A;  Init G <= A;  stable (Acts G) A |] \
-\      ==> Invariant (F Join G) A";
+\     ==> Invariant (F Join G) A";
 by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
 				  stable_Join]) 1);
 by (force_tac(claset() addIs [stable_reachable, stable_Int],