# HG changeset patch
# User paulson
# Date 927105694 -7200
# Node ID 8542c6dda828a90618177b5dd6d1fa2190ae733c
# Parent  677713791bd82d38a6e1906d7715a9f3af9f8c7d
new theorem Always_reachable

diff -r 677713791bd8 -r 8542c6dda828 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Tue May 18 15:52:34 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Wed May 19 11:21:34 1999 +0200
@@ -267,6 +267,8 @@
 by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
 qed "invariant_imp_Always";
 
+bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always);
+
 Goal "Always A = {F. F : invariant (reachable F Int A)}";
 by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def, 
 				  Constrains_eq_constrains, stable_def]) 1);