1.1 --- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 15:01:20 2012 +0200
1.2 +++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy Wed Oct 10 15:17:40 2012 +0200
1.3 @@ -273,7 +273,7 @@
1.4
1.5
1.6 lemma embed_underS:
1.7 -assumes WELL: "Well_order r" and WELL: "Well_order r'" and
1.8 +assumes WELL: "Well_order r" and WELL': "Well_order r'" and
1.9 EMB: "embed r r' f" and IN: "a \<in> Field r"
1.10 shows "bij_betw f (rel.underS r a) (rel.underS r' (f a))"
1.11 proof-
2.1 --- a/src/HOL/NthRoot.thy Wed Oct 10 15:01:20 2012 +0200
2.2 +++ b/src/HOL/NthRoot.thy Wed Oct 10 15:17:40 2012 +0200
2.3 @@ -398,9 +398,9 @@
2.4
2.5 lemma DERIV_real_root_generic:
2.6 assumes "0 < n" and "x \<noteq> 0"
2.7 - and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
2.8 - and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
2.9 - and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
2.10 + and "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
2.11 + and "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
2.12 + and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
2.13 shows "DERIV (root n) x :> D"
2.14 using assms by (cases "even n", cases "0 < x",
2.15 auto intro: DERIV_real_root[THEN DERIV_cong]