src/HOL/SMT/SMT_Base.thy
changeset 36884 88cf4896b980
parent 36084 3176ec2244ad
child 36891 e0d295cb8bfd
--- 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"