src/ZF/OrderArith.thy
changeset 13823 d49ffd9f9662
parent 13784 b9f6154427a4
child 14120 3a73850c6c7d
     1.1 --- a/src/ZF/OrderArith.thy	Tue Feb 18 19:13:47 2003 +0100
     1.2 +++ b/src/ZF/OrderArith.thy	Wed Feb 19 10:53:27 2003 +0100
     1.3 @@ -49,10 +49,12 @@
     1.4      "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
     1.5  by (unfold radd_def, blast)
     1.6  
     1.7 -lemma radd_Inr_Inl_iff [iff]: 
     1.8 -    "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
     1.9 +lemma radd_Inr_Inl_iff [simp]: 
    1.10 +    "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
    1.11  by (unfold radd_def, blast)
    1.12  
    1.13 +declare radd_Inr_Inl_iff [THEN iffD1, dest!] 
    1.14 +
    1.15  subsubsection{*Elimination Rule*}
    1.16  
    1.17  lemma raddE: