# HG changeset patch
# User haftmann
# Date 1560501267 0
# Node ID e54caaa38ad991b50d38c7b7e0fcef5ae6330547
# Parent  e4d626692640452c2ff3314b8f66d81b141ef04e
removed outcommented example which seems not to work as advertized

diff -r e4d626692640 -r e54caaa38ad9 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Fields.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -904,20 +904,6 @@
 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
 explosions.\<close>
 
-(* Only works once linear arithmetic is installed:
-text{*An example:*}
-lemma fixes a b c d e f :: "'a::linordered_field"
-shows "\<lbrakk>a>b; c<d; e<f; 0 < u \<rbrakk> \<Longrightarrow>
- ((a-b)*(c-d)*(e-f))/((c-d)*(e-f)*(a-b)) <
- ((e-f)*(a-b)*(c-d))/((e-f)*(a-b)*(c-d)) + u"
-apply(subgoal_tac "(c-d)*(e-f)*(a-b) > 0")
- prefer 2 apply(simp add:sign_simps)
-apply(subgoal_tac "(c-d)*(e-f)*(a-b)*u > 0")
- prefer 2 apply(simp add:sign_simps)
-apply(simp add:field_simps)
-done
-*)
-
 lemma divide_pos_pos[simp]:
   "0 < x ==> 0 < y ==> 0 < x / y"
 by(simp add:field_simps)