# HG changeset patch
# User wenzelm
# Date 1349875060 -7200
# Node ID a344f1a2121184b3886635d5c67c1b6fc8c90a49
# Parent  2bbb0013ff82182afe38b2e323cc0b18b0ff752a
eliminated spurious fact duplicates;

diff -r 2bbb0013ff82 -r a344f1a21211 src/HOL/Cardinals/Wellorder_Embedding_Base.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Wed Oct 10 15:01:20 2012 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Wed Oct 10 15:17:40 2012 +0200
@@ -273,7 +273,7 @@
 
 
 lemma embed_underS:
-assumes WELL: "Well_order r" and WELL: "Well_order r'" and
+assumes WELL: "Well_order r" and WELL': "Well_order r'" and
         EMB: "embed r r' f" and IN: "a \<in> Field r"
 shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
 proof-
diff -r 2bbb0013ff82 -r a344f1a21211 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Wed Oct 10 15:01:20 2012 +0200
+++ b/src/HOL/NthRoot.thy	Wed Oct 10 15:17:40 2012 +0200
@@ -398,9 +398,9 @@
 
 lemma DERIV_real_root_generic:
   assumes "0 < n" and "x \<noteq> 0"
-  and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
-  and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
-  and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+    and "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+    and "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
+    and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
   shows "DERIV (root n) x :> D"
 using assms by (cases "even n", cases "0 < x",
   auto intro: DERIV_real_root[THEN DERIV_cong]