# HG changeset patch
# User boehmes
# Date 1273701228 -7200
# Node ID 88cf4896b980096c8162f0c377622b0f150c390c
# Parent  d7085f0ec087ced28fe9c1322368e606ec4c9094
moved the addition of DLO tactic into the Z3 theory (DLO is required only for Z3 proof reconstruction)

diff -r d7085f0ec087 -r 88cf4896b980 src/HOL/SMT/SMT_Base.thy
--- 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"
diff -r d7085f0ec087 -r 88cf4896b980 src/HOL/SMT/Z3.thy
--- a/src/HOL/SMT/Z3.thy	Wed May 12 17:10:53 2010 +0200
+++ b/src/HOL/SMT/Z3.thy	Wed May 12 23:53:48 2010 +0200
@@ -5,7 +5,7 @@
 header {* Binding to the SMT solver Z3, with proof reconstruction *}
 
 theory Z3
-imports SMT_Base
+imports SMT_Base "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
 uses
   "Tools/z3_proof_terms.ML"
   "Tools/z3_proof_rules.ML"
@@ -15,7 +15,11 @@
   "Tools/z3_solver.ML"
 begin
 
-setup {* Z3_Proof_Rules.setup #> Z3_Solver.setup *}
+setup {*
+  Z3_Proof_Rules.setup #>
+  Z3_Solver.setup #>
+  Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac)
+*}
 
 lemmas [z3_rewrite] =
   refl eq_commute conj_commute disj_commute simp_thms nnf_simps