src/HOL/UNITY/UNITY.thy
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*}