tuned;
authorwenzelm
Sun May 03 16:45:07 2015 +0200 (2015-05-03)
changeset 60241cde717a55db7
parent 60240 3f61058a2de6
child 60242 3a8501876dba
tuned;
src/HOL/Binomial.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Binomial.thy	Sun May 03 16:44:38 2015 +0200
     1.2 +++ b/src/HOL/Binomial.thy	Sun May 03 16:45:07 2015 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    by (induct n) (auto simp: le_Suc_eq)
     1.5  
     1.6  context
     1.7 -  fixes XXX :: "'a :: {semiring_char_0,linordered_semidom,semiring_no_zero_divisors}"
     1.8 +  assumes "SORT_CONSTRAINT('a::linordered_semidom)"
     1.9  begin
    1.10    
    1.11    lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
    1.12 @@ -79,8 +79,7 @@
    1.13    by (induct n) (auto simp: less_Suc_eq)
    1.14  
    1.15  lemma fact_less_mono:
    1.16 -  fixes XXX :: "'a :: {semiring_char_0,linordered_semidom,semiring_no_zero_divisors}"
    1.17 -  shows "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: 'a)"
    1.18 +  "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: 'a::linordered_semidom)"
    1.19    by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat)
    1.20  
    1.21  lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
     2.1 --- a/src/HOL/Transcendental.thy	Sun May 03 16:44:38 2015 +0200
     2.2 +++ b/src/HOL/Transcendental.thy	Sun May 03 16:45:07 2015 +0200
     2.3 @@ -987,8 +987,7 @@
     2.4    unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
     2.5  
     2.6  lemma exp_fdiffs:
     2.7 -  fixes XXX :: "'a::{real_normed_field,banach}"
     2.8 -  shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))"
     2.9 +  "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a::{real_normed_field,banach}))"
    2.10    by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
    2.11             del: mult_Suc of_nat_Suc)
    2.12  
    2.13 @@ -3758,8 +3757,7 @@
    2.14    where "tan = (\<lambda>x. sin x / cos x)"
    2.15  
    2.16  lemma tan_of_real:
    2.17 -  fixes XXX :: "'a::{real_normed_field,banach}"
    2.18 -  shows  "of_real(tan x) = (tan(of_real x) :: 'a)"
    2.19 +  "of_real (tan x) = (tan (of_real x) :: 'a::{real_normed_field,banach})"
    2.20    by (simp add: tan_def sin_of_real cos_of_real)
    2.21  
    2.22  lemma tan_in_Reals [simp]: