--- a/src/HOL/Binomial.thy Sun May 03 16:44:38 2015 +0200
+++ b/src/HOL/Binomial.thy Sun May 03 16:45:07 2015 +0200
@@ -39,7 +39,7 @@
by (induct n) (auto simp: le_Suc_eq)
context
- fixes XXX :: "'a :: {semiring_char_0,linordered_semidom,semiring_no_zero_divisors}"
+ assumes "SORT_CONSTRAINT('a::linordered_semidom)"
begin
lemma fact_mono: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: 'a)"
@@ -79,8 +79,7 @@
by (induct n) (auto simp: less_Suc_eq)
lemma fact_less_mono:
- fixes XXX :: "'a :: {semiring_char_0,linordered_semidom,semiring_no_zero_divisors}"
- shows "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: 'a)"
+ "\<lbrakk>0 < m; m < n\<rbrakk> \<Longrightarrow> fact m < (fact n :: 'a::linordered_semidom)"
by (metis of_nat_fact of_nat_less_iff fact_less_mono_nat)
lemma fact_ge_Suc_0_nat [simp]: "fact n \<ge> Suc 0"
--- a/src/HOL/Transcendental.thy Sun May 03 16:44:38 2015 +0200
+++ b/src/HOL/Transcendental.thy Sun May 03 16:45:07 2015 +0200
@@ -987,8 +987,7 @@
unfolding exp_def by (rule summable_exp_generic [THEN summable_sums])
lemma exp_fdiffs:
- fixes XXX :: "'a::{real_normed_field,banach}"
- shows "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a))"
+ "diffs (\<lambda>n. inverse (fact n)) = (\<lambda>n. inverse (fact n :: 'a::{real_normed_field,banach}))"
by (simp add: diffs_def mult_ac nonzero_inverse_mult_distrib nonzero_of_real_inverse
del: mult_Suc of_nat_Suc)
@@ -3758,8 +3757,7 @@
where "tan = (\<lambda>x. sin x / cos x)"
lemma tan_of_real:
- fixes XXX :: "'a::{real_normed_field,banach}"
- shows "of_real(tan x) = (tan(of_real x) :: 'a)"
+ "of_real (tan x) = (tan (of_real x) :: 'a::{real_normed_field,banach})"
by (simp add: tan_def sin_of_real cos_of_real)
lemma tan_in_Reals [simp]: