src/HOL/UNITY/UNITY.thy

 lemma stable_constrains_Int: 
   "[| F \<in> stable C; F \<in>  (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
 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*}
 
 lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"