src/HOL/UNITY/Union.thy
changeset 45605 a89b4bc311a5
parent 44928 7ef6505bde7f
child 46577 e5438c5797ae
     1.1 --- a/src/HOL/UNITY/Union.thy	Sun Nov 20 20:59:30 2011 +0100
     1.2 +++ b/src/HOL/UNITY/Union.thy	Sun Nov 20 21:05:23 2011 +0100
     1.3 @@ -332,7 +332,7 @@
     1.4  lemma ok_commute: "(F ok G) = (G ok F)"
     1.5  by (auto simp add: ok_def)
     1.6  
     1.7 -lemmas ok_sym = ok_commute [THEN iffD1, standard]
     1.8 +lemmas ok_sym = ok_commute [THEN iffD1]
     1.9  
    1.10  lemma ok_iff_OK:
    1.11       "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"