equal
deleted
inserted
replaced
144 by dlo |
144 by dlo |
145 |
145 |
146 lemma "\<forall>(a::'a::ordered_field) b. (\<exists>x. a < x \<and> x< b) \<longleftrightarrow> (a < b)" |
146 lemma "\<forall>(a::'a::ordered_field) b. (\<exists>x. a < x \<and> x< b) \<longleftrightarrow> (a < b)" |
147 by dlo |
147 by dlo |
148 |
148 |
149 section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see Arith_Tools.thy *} |
149 section {* Contructive dense linear orders yield QE for linear arithmetic over ordered Fields -- see @{text "Arith_Tools.thy"} *} |
150 |
150 |
151 context Linorder |
151 context Linorder |
152 begin |
152 begin |
153 |
153 |
154 text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*} |
154 text{* Theorems for @{text "\<exists>z. \<forall>x. x \<sqsubset> z \<longrightarrow> (P x \<longleftrightarrow> P\<^bsub>-\<infinity>\<^esub>)"}*} |