| changeset 6672 | 8542c6dda828 |
| parent 6575 | 70d758762c50 |
| child 6704 | 5febcf428342 |
--- 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);