Tuned document
authorchaieb
Tue Jul 31 09:31:19 2007 +0200 (2007-07-31)
changeset 2408184a5a6267d60
parent 24080 8c67d869531b
child 24082 2811a7c0f3b1
Tuned document
src/HOL/Dense_Linear_Order.thy
     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