changeset 53215 | 5e47c31c6f7c |
parent 52435 | 6646bb548c6b |
child 53374 | a14d2a854c02 |
--- a/src/HOL/Fields.thy Mon Aug 26 23:39:53 2013 +0200 +++ b/src/HOL/Fields.thy Tue Aug 27 14:37:56 2013 +0200 @@ -842,7 +842,7 @@ lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b" by (simp add: field_simps zero_less_two) -subclass dense_linorder +subclass unbounded_dense_linorder proof fix x y :: 'a from less_add_one show "\<exists>y. x < y" ..