--- a/src/HOL/SMT/SMT_Base.thy Wed May 12 17:10:53 2010 +0200
+++ b/src/HOL/SMT/SMT_Base.thy Wed May 12 23:53:48 2010 +0200
@@ -6,7 +6,6 @@
theory SMT_Base
imports Real "~~/src/HOL/Word/Word"
- "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
uses
"~~/src/Tools/cache_io.ML"
("Tools/smt_normalize.ML")
@@ -41,6 +40,7 @@
where "trigger _ P = P"
+
section {* Arithmetic *}
text {*
@@ -53,11 +53,6 @@
where "a rem b =
(if (a \<ge> 0 \<and> b < 0) \<or> (a < 0 \<and> b \<ge> 0) then - (a mod b) else a mod b)"
-text {* A decision procedure for linear real arithmetic: *}
-
-setup {*
- Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac)
-*}
section {* Bitvectors *}
@@ -87,6 +82,7 @@
where "bv_ashr w1 w2 = (w1 >>> unat w2)"
+
section {* Higher-Order Encoding *}
definition "apply" where "apply f x = f x"
@@ -104,6 +100,7 @@
ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_upd_eq apply_def
+
section {* First-order logic *}
text {*
@@ -130,6 +127,7 @@
"(x iff y) = (x = y)"
+
section {* Setup *}
use "Tools/smt_normalize.ML"