# 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) "\<forall>a b. (\<exists>x. a \<sqsubset> x \<and> x\<sqsubset> b) \<longleftrightarrow> (a \<sqsubset> b)"
-  by dlo
-
-lemma "\<forall>(a::'a::ordered_field) b. (\<exists>x. a < x \<and> x< b) \<longleftrightarrow> (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