author chaieb Tue Jul 31 09:31:19 2007 +0200 (2007-07-31) changeset 24081 84a5a6267d60 parent 24080 8c67d869531b child 24082 2811a7c0f3b1
Tuned document
```     1.1 --- a/src/HOL/Dense_Linear_Order.thy	Tue Jul 31 00:56:34 2007 +0200
1.2 +++ b/src/HOL/Dense_Linear_Order.thy	Tue Jul 31 09:31:19 2007 +0200
1.3 @@ -124,7 +124,6 @@
1.4  lemmas dnf_simps = weak_dnf_simps nnf_simps ex_distrib
1.5
1.6  use "Tools/Qelim/langford.ML"
1.7 -
1.8  method_setup dlo = {*
1.9    Method.ctxt_args (Method.SIMPLE_METHOD' o LangfordQE.dlo_tac)
1.10  *} "Langford's algorithm for quantifier elimination in dense linear orders"
1.11 @@ -140,12 +139,6 @@
1.12  apply (rule gt_half_sum, simp)
1.13  done
1.14
1.15 -lemma (in dense_linear_order) "\<forall>a b. (\<exists>x. a \<sqsubset> x \<and> x\<sqsubset> b) \<longleftrightarrow> (a \<sqsubset> b)"
1.16 -  by dlo
1.17 -
1.18 -lemma "\<forall>(a::'a::ordered_field) b. (\<exists>x. a < x \<and> x< b) \<longleftrightarrow> (a < b)"
1.19 -  by dlo
1.20 -
1.21  section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *}
1.22
1.23  context Linorder
1.24 @@ -561,4 +554,4 @@
1.25    Method.ctxt_args (Method.SIMPLE_METHOD' o FerranteRackoff.dlo_tac)
1.26  *} "Ferrante and Rackoff's algorithm for quantifier elimination in dense linear orders"
1.27
1.28 -end
1.29 +end
```