src/HOL/SMT.thy
changeset 56078 624faeda77b5
parent 56046 683148f3ae48
child 57213 9daec42f6784
     1.1 --- a/src/HOL/SMT.thy	Thu Mar 13 08:56:08 2014 +0100
     1.2 +++ b/src/HOL/SMT.thy	Thu Mar 13 13:18:13 2014 +0100
     1.3 @@ -31,14 +31,13 @@
     1.4  quantifier block.
     1.5  *}
     1.6  
     1.7 -datatype pattern = Pattern
     1.8 +typedecl pattern
     1.9  
    1.10 -definition pat :: "'a \<Rightarrow> pattern" where "pat _ = Pattern"
    1.11 -definition nopat :: "'a \<Rightarrow> pattern" where "nopat _ = Pattern"
    1.12 +consts
    1.13 +  pat :: "'a \<Rightarrow> pattern"
    1.14 +  nopat :: "'a \<Rightarrow> pattern"
    1.15  
    1.16 -definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool"
    1.17 -where "trigger _ P = P"
    1.18 -
    1.19 +definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P"
    1.20  
    1.21  
    1.22  subsection {* Quantifier weights *}
    1.23 @@ -67,7 +66,6 @@
    1.24  *}
    1.25  
    1.26  
    1.27 -
    1.28  subsection {* Higher-order encoding *}
    1.29  
    1.30  text {*
    1.31 @@ -88,7 +86,6 @@
    1.32    fun_upd_upd fun_app_def
    1.33  
    1.34  
    1.35 -
    1.36  subsection {* First-order logic *}
    1.37  
    1.38  text {*
    1.39 @@ -107,7 +104,6 @@
    1.40  definition term_false where "term_false = False"
    1.41  
    1.42  
    1.43 -
    1.44  subsection {* Integer division and modulo for Z3 *}
    1.45  
    1.46  definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.47 @@ -117,7 +113,6 @@
    1.48    "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
    1.49  
    1.50  
    1.51 -
    1.52  subsection {* Setup *}
    1.53  
    1.54  ML_file "Tools/SMT/smt_builtin.ML"
    1.55 @@ -426,7 +421,7 @@
    1.56  
    1.57  
    1.58  hide_type (open) pattern
    1.59 -hide_const Pattern fun_app term_true term_false z3div z3mod
    1.60 +hide_const fun_app term_true term_false z3div z3mod
    1.61  hide_const (open) trigger pat nopat weight
    1.62  
    1.63  end