# HG changeset patch
# User wenzelm
# Date 1430664307 -7200
# Node ID cde717a55db7cdfa79c3951acc1f378a5ac9b67f
# Parent  3f61058a2de65ba8c5032417ff246842b19dd2f8
tuned;

diff -r 3f61058a2de6 -r cde717a55db7 src/HOL/Binomial.thy
--- 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"
diff -r 3f61058a2de6 -r cde717a55db7 src/HOL/Transcendental.thy
--- 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]: