changeset 45605 | a89b4bc311a5 |
parent 36866 | 426d5781bb25 |
child 45694 | 4a8743618257 |
--- a/src/HOL/UNITY/UNITY.thy Sun Nov 20 20:59:30 2011 +0100 +++ b/src/HOL/UNITY/UNITY.thy Sun Nov 20 21:05:23 2011 +0100 @@ -274,7 +274,7 @@ by (unfold stable_def constrains_def, blast) (*[| F \<in> stable C; F \<in> (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *) -lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard] +lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI] subsubsection{*invariant*}