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 {*
-*}

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"```