--- a/src/HOL/SMT.thy Wed May 12 23:54:02 2010 +0200
+++ b/src/HOL/SMT.thy Wed May 12 23:54:04 2010 +0200
@@ -8,7 +8,6 @@
imports List
uses
"~~/src/Tools/cache_io.ML"
- ("Tools/SMT/smt_additional_facts.ML")
("Tools/SMT/smt_monomorph.ML")
("Tools/SMT/smt_normalize.ML")
("Tools/SMT/smt_translate.ML")
@@ -122,12 +121,10 @@
section {* Configuration *}
text {*
-The current configuration can be printed by the following command
-(which shows the values of most options):
+The current configuration can be printed by the command
+@{text smt_status}, which shows the values of most options.
*}
-smt_status
-
subsection {* General configuration options *}
@@ -294,13 +291,4 @@
"x + y = y + x"
by auto
-lemma [z3_rule]:
- "0 + (x::real) = x"
- "x + 0 = x"
- "0 * x = 0"
- "1 * x = x"
- "x + y = y + x"
- by auto
-
-
end