# HG changeset patch
# User paulson
# Date 937816929 -7200
# Node ID 1a7a38d8f5bd682ebf1afff8e49b86d369733b24
# Parent  8af61a565a4a84c7923434907edc5dd58ca9956b
new theorem Always_INT_distrib; therefore renamed Always_Int
to Always_Int_I

diff -r 8af61a565a4a -r 1a7a38d8f5bd src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Mon Sep 20 10:40:40 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Mon Sep 20 10:42:09 1999 +0200
@@ -319,21 +319,29 @@
 
 (** Conjoining Always properties **)
 
+Goal "Always (A Int B) = Always A Int Always B";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_Int_distrib";
+
+Goal "Always (INTER I A) = (INT i:I. Always (A i))";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_INT_distrib";
+
 Goal "[| F : Always A;  F : Always B |] ==> F : Always (A Int B)";
 by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
-qed "Always_Int";
+qed "Always_Int_I";
 
 (*Delete the nearest invariance assumption (which will be the second one
-  used by Always_Int) *)
+  used by Always_Int_I) *)
 val Always_thin =
     read_instantiate_sg (sign_of thy)
                 [("V", "?F : Always ?A")] thin_rl;
 
 (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
-val Always_Int_tac = dtac Always_Int THEN' assume_tac THEN' etac Always_thin;
+val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
 
 (*Combines a list of invariance THEOREMS into one.*)
-val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int);
+val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
 
 
 (*To allow expansion of the program's definition when appropriate*)