--- a/src/ZF/OrderArith.thy Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/OrderArith.thy Wed Feb 19 10:53:27 2003 +0100
@@ -49,10 +49,12 @@
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s"
by (unfold radd_def, blast)
-lemma radd_Inr_Inl_iff [iff]:
- "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
+lemma radd_Inr_Inl_iff [simp]:
+ "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
by (unfold radd_def, blast)
+declare radd_Inr_Inl_iff [THEN iffD1, dest!]
+
subsubsection{*Elimination Rule*}
lemma raddE: