# HG changeset patch
# User paulson
# Date 927796785 -7200
# Node ID 66e4118eead972ddf8fbb0c64fec9fd7f5fae732
# Parent  06189132c67b4662cf965b5d74ed569945046759
replaced rules Always_ConstrainsI/D by equivalences Always_Constrains_pre,
Always_Constrains_post

diff -r 06189132c67b -r 66e4118eead9 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Thu May 27 10:13:52 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Thu May 27 11:19:45 1999 +0200
@@ -296,24 +296,23 @@
 
 (*** "Co" rules involving Always ***)
 
-Goal "[| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A'";
-by (asm_full_simp_tac
+Goal "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')";
+by (asm_simp_tac
     (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
 			 Constrains_def, Int_assoc RS sym]) 1);
-qed "Always_ConstrainsI";
+qed "Always_Constrains_pre";
 
-(* [| F : Always INV; F : (INV Int A) Co A |]
-   ==> F : Stable A *)
-bind_thm ("Always_StableI", Always_ConstrainsI RS StableI);
-
-Goal "[| F : Always INV;  F : A Co A' |]   \
-\     ==> F : A Co (INV Int A')";
-by (asm_full_simp_tac
+Goal "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')";
+by (asm_simp_tac
     (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
 			 Constrains_eq_constrains, Int_assoc RS sym]) 1);
-qed "Always_ConstrainsD";
+qed "Always_Constrains_post";
 
-bind_thm ("Always_StableD", StableD RSN (2,Always_ConstrainsD));
+(* [| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A' *)
+bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1);
+
+(* [| F : Always INV;  F : A Co A' |] ==> F : A Co (INV Int A') *)
+bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);
 
 
 
@@ -352,3 +351,4 @@
 	      ALLGOALS Asm_full_simp_tac]) i;
 
 
+leadsTo_wf_induct
\ No newline at end of file