--- a/src/HOL/SMT.thy Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/SMT.thy Thu Mar 13 13:18:13 2014 +0100
@@ -31,14 +31,13 @@
quantifier block.
*}
-datatype pattern = Pattern
+typedecl pattern
-definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
-definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
+consts
+ pat :: "'a \<Rightarrow> pattern"
+ nopat :: "'a \<Rightarrow> pattern"
-definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
-where "trigger _ P = P"
-
+definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P"
subsection {* Quantifier weights *}
@@ -67,7 +66,6 @@
*}
-
subsection {* Higher-order encoding *}
text {*
@@ -88,7 +86,6 @@
fun_upd_upd fun_app_def
-
subsection {* First-order logic *}
text {*
@@ -107,7 +104,6 @@
definition term_false where "term_false = False"
-
subsection {* Integer division and modulo for Z3 *}
definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
@@ -117,7 +113,6 @@
"z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
-
subsection {* Setup *}
ML_file "Tools/SMT/smt_builtin.ML"
@@ -426,7 +421,7 @@
hide_type (open) pattern
-hide_const Pattern fun_app term_true term_false z3div z3mod
+hide_const fun_app term_true term_false z3div z3mod
hide_const (open) trigger pat nopat weight
end