removed outcommented example which seems not to work as advertized
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (5 weeks ago ago)
changeset 70528e54caaa38ad9
parent 70527 e4d626692640
child 70529 050104f01bf9
removed outcommented example which seems not to work as advertized
src/HOL/Fields.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 @@ -904,20 +904,6 @@
     1.4  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.5  explosions.\<close>
     1.6  
     1.7 -(* Only works once linear arithmetic is installed:
     1.8 -text{*An example:*}
     1.9 -lemma fixes a b c d e f :: "'a::linordered_field"
    1.10 -shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
    1.11 - ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
    1.12 - ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
    1.13 -apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
    1.14 - prefer 2 apply(simp add:sign_simps)
    1.15 -apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
    1.16 - prefer 2 apply(simp add:sign_simps)
    1.17 -apply(simp add:field_simps)
    1.18 -done
    1.19 -*)
    1.20 -
    1.21  lemma divide_pos_pos[simp]:
    1.22    "0 < x ==> 0 < y ==> 0 < x / y"
    1.23  by(simp add:field_simps)