# 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 \ 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 \ 0" - and even: "\ even n ; 0 < x \ \ D = inverse (real n * root n x ^ (n - Suc 0))" - and even: "\ even n ; x < 0 \ \ D = - inverse (real n * root n x ^ (n - Suc 0))" - and odd: "odd n \ D = inverse (real n * root n x ^ (n - Suc 0))" + and "\ even n ; 0 < x \ \ D = inverse (real n * root n x ^ (n - Suc 0))" + and "\ even n ; x < 0 \ \ D = - inverse (real n * root n x ^ (n - Suc 0))" + and "odd n \ 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]