src/HOL/Groups.thy
changeset 54147 97a8ff4e4ac9
parent 52435 6646bb548c6b
child 54148 c8cc5ab4a863
     1.1 --- a/src/HOL/Groups.thy	Fri Oct 18 10:35:57 2013 +0200
     1.2 +++ b/src/HOL/Groups.thy	Fri Oct 18 10:43:20 2013 +0200
     1.3 @@ -1341,7 +1341,7 @@
     1.4  
     1.5  subsection {* Tools setup *}
     1.6  
     1.7 -lemma add_mono_thms_linordered_semiring [no_atp]:
     1.8 +lemma add_mono_thms_linordered_semiring:
     1.9    fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add"
    1.10    shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    1.11      and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l"
    1.12 @@ -1349,7 +1349,7 @@
    1.13      and "i = j \<and> k = l \<Longrightarrow> i + k = j + l"
    1.14  by (rule add_mono, clarify+)+
    1.15  
    1.16 -lemma add_mono_thms_linordered_field [no_atp]:
    1.17 +lemma add_mono_thms_linordered_field:
    1.18    fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add"
    1.19    shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l"
    1.20      and "i = j \<and> k < l \<Longrightarrow> i + k < j + l"