src/HOL/Sum_Type.thy
changeset 17084 fb0a80aef0be
parent 17026 43cc86fd3536
child 19008 14c1b2f5dda4
     1.1 --- a/src/HOL/Sum_Type.thy	Tue Aug 16 13:54:24 2005 +0200
     1.2 +++ b/src/HOL/Sum_Type.thy	Tue Aug 16 15:36:28 2005 +0200
     1.3 @@ -78,7 +78,8 @@
     1.4  apply (rule Inr_RepI)
     1.5  done
     1.6  
     1.7 -lemmas Inr_not_Inl = Inl_not_Inr [THEN not_sym, standard, iff]
     1.8 +lemmas Inr_not_Inl = Inl_not_Inr [THEN not_sym, standard]
     1.9 +declare Inr_not_Inl [iff]
    1.10  
    1.11  lemmas Inl_neq_Inr = Inl_not_Inr [THEN notE, standard]
    1.12  lemmas Inr_neq_Inl = sym [THEN Inl_neq_Inr, standard]