# HG changeset patch
# User paulson
# Date 1045648407 -3600
# Node ID d49ffd9f9662dae87fa012668931ea6e92a38d42
# Parent  bb5eda7416e5aa06649ad9ff28bf0208c04e7049
fixed anomalies in the installed classical rules

diff -r bb5eda7416e5 -r d49ffd9f9662 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/Nat.thy	Wed Feb 19 10:53:27 2003 +0100
@@ -113,11 +113,11 @@
 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
 by (induct a rule: nat_induct, auto)
 
-lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
+lemma succ_natD: "succ(i): nat ==> i: nat"
 by (rule Ord_trans [OF succI1], auto)
 
 lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
-by blast
+by (blast dest!: succ_natD)
 
 lemma nat_le_Limit: "Limit(i) ==> nat le i"
 apply (rule subset_imp_le)
diff -r bb5eda7416e5 -r d49ffd9f9662 src/ZF/OrderArith.thy
--- 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:
diff -r bb5eda7416e5 -r d49ffd9f9662 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/QPair.thy	Wed Feb 19 10:53:27 2003 +0100
@@ -233,10 +233,10 @@
 lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
 by (simp add: qsum_defs )
 
-lemma QInl_QInr_iff [iff]: "QInl(a)=QInr(b) <-> False"
+lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False"
 by (simp add: qsum_defs )
 
-lemma QInr_QInl_iff [iff]: "QInr(b)=QInl(a) <-> False"
+lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False"
 by (simp add: qsum_defs )
 
 lemma qsum_empty [simp]: "0<+>0 = 0"
@@ -246,8 +246,8 @@
 
 lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
 lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
-lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE]
-lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE]
+lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
+lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
 
 lemma QInlD: "QInl(a): A<+>B ==> a: A"
 by blast
diff -r bb5eda7416e5 -r d49ffd9f9662 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/Sum.thy	Wed Feb 19 10:53:27 2003 +0100
@@ -90,10 +90,10 @@
 lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
 by (simp add: sum_defs)
 
-lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False"
+lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) <-> False"
 by (simp add: sum_defs)
 
-lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False"
+lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) <-> False"
 by (simp add: sum_defs)
 
 lemma sum_empty [simp]: "0+0 = 0"
@@ -103,8 +103,8 @@
 
 lemmas Inl_inject = Inl_iff [THEN iffD1, standard]
 lemmas Inr_inject = Inr_iff [THEN iffD1, standard]
-lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE]
-lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE]
+lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
+lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]
 
 
 lemma InlD: "Inl(a): A+B ==> a: A"