moved comment to approproiate place
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (5 weeks ago ago)
changeset 70529050104f01bf9
parent 70528 e54caaa38ad9
child 70530 80a1aa30e24d
moved comment to approproiate place
src/HOL/Fields.thy
src/HOL/Rat.thy
     1.1 --- a/src/HOL/Fields.thy	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/src/HOL/Fields.thy	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -900,10 +900,6 @@
     1.4    "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z - w * y) / (y * z) \<le> 0"
     1.5    by (subst le_iff_diff_le_0) (simp add: diff_frac_eq )
     1.6  
     1.7 -text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
     1.8 -of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
     1.9 -explosions.\<close>
    1.10 -
    1.11  lemma divide_pos_pos[simp]:
    1.12    "0 < x ==> 0 < y ==> 0 < x / y"
    1.13  by(simp add:field_simps)
     2.1 --- a/src/HOL/Rat.thy	Fri Jun 14 08:34:27 2019 +0000
     2.2 +++ b/src/HOL/Rat.thy	Fri Jun 14 08:34:27 2019 +0000
     2.3 @@ -529,6 +529,10 @@
     2.4  
     2.5  end
     2.6  
     2.7 +text\<open>Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs
     2.8 +of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> because the former can lead to case
     2.9 +explosions.\<close>
    2.10 +
    2.11  lemmas (in linordered_field) sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
    2.12  lemmas sign_simps = algebra_simps zero_less_mult_iff mult_less_0_iff
    2.13