--- a/src/HOL/UNITY/Constrains.ML Mon Mar 01 18:37:52 1999 +0100
+++ b/src/HOL/UNITY/Constrains.ML Mon Mar 01 18:38:43 1999 +0100
@@ -89,25 +89,24 @@
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "ball_Constrains_INT";
-Goal "[| F : Constrains A A'; A <= reachable F |] ==> A <= A'";
+Goal "F : Constrains A A' ==> reachable F Int A <= A'";
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
by (dtac constrains_imp_subset 1);
-by (auto_tac (claset() addIs [impOfSubs reachable_subset_States],
- simpset() addsimps [Int_subset_iff, Int_lower1]));
+by (ALLGOALS
+ (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1])));
qed "Constrains_imp_subset";
Goalw [Constrains_def]
"[| F : Constrains A B; F : Constrains B C |] \
\ ==> F : Constrains A C";
-by (blast_tac (claset() addIs [impOfSubs reachable_subset_States,
- constrains_trans, constrains_weaken]) 1);
+by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
qed "Constrains_trans";
-Goal "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
-\ ==> F : Constrains A (A' Un B')";
-by (asm_full_simp_tac (simpset() addsimps [Constrains_def, Int_Un_distrib]) 1);
-by (blast_tac (claset() addIs [impOfSubs reachable_subset_States,
- constrains_cancel]) 1);
+Goalw [Constrains_def, constrains_def]
+ "[| F : Constrains A (A' Un B); F : Constrains B B' |] \
+\ ==> F : Constrains A (A' Un B')";
+by (Clarify_tac 1);
+by (Blast_tac 1);
qed "Constrains_cancel";