# HG changeset patch # User chaieb # Date 1185867079 -7200 # Node ID 84a5a6267d60442c57bbfb3bb6243b23504501cd # Parent 8c67d869531b0831fe2e722e443463ed30d45702 Tuned document diff -r 8c67d869531b -r 84a5a6267d60 src/HOL/Dense_Linear_Order.thy --- a/src/HOL/Dense_Linear_Order.thy Tue Jul 31 00:56:34 2007 +0200 +++ b/src/HOL/Dense_Linear_Order.thy Tue Jul 31 09:31:19 2007 +0200 @@ -124,7 +124,6 @@ lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib use "Tools/Qelim/langford.ML" - method_setup dlo = {* Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac) *} "Langford's algorithm for quantifier elimination in dense linear orders" @@ -140,12 +139,6 @@ apply (rule gt_half_sum, simp) done -lemma (in dense_linear_order) "\a b. (\x. a \ x \ x\ b) \ (a \ b)" - by dlo - -lemma "\(a::'a::ordered_field) b. (\x. a < x \ x< b) \ (a < b)" - by dlo - section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} context Linorder @@ -561,4 +554,4 @@ Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac) *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders" -end +end