src/HOL/SMT.thy
changeset 41426 09615ed31f04
parent 41328 6792a5c92a58
child 41432 3214c39777ab
     1.1 --- a/src/HOL/SMT.thy	Fri Dec 31 00:11:24 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Jan 03 16:22:08 2011 +0100
     1.3 @@ -5,14 +5,14 @@
     1.4  header {* Bindings to Satisfiability Modulo Theories (SMT) solvers *}
     1.5  
     1.6  theory SMT
     1.7 -imports List
     1.8 +imports Record
     1.9  uses
    1.10 -  "Tools/Datatype/datatype_selectors.ML"
    1.11    "Tools/SMT/smt_utils.ML"
    1.12    "Tools/SMT/smt_failure.ML"
    1.13    "Tools/SMT/smt_config.ML"
    1.14    ("Tools/SMT/smt_monomorph.ML")
    1.15    ("Tools/SMT/smt_builtin.ML")
    1.16 +  ("Tools/SMT/smt_datatypes.ML")
    1.17    ("Tools/SMT/smt_normalize.ML")
    1.18    ("Tools/SMT/smt_translate.ML")
    1.19    ("Tools/SMT/smt_solver.ML")
    1.20 @@ -123,7 +123,6 @@
    1.21  
    1.22  
    1.23  
    1.24 -
    1.25  subsection {* Integer division and modulo for Z3 *}
    1.26  
    1.27  definition z3div :: "int \<Rightarrow> int \<Rightarrow> int" where
    1.28 @@ -138,6 +137,7 @@
    1.29  
    1.30  use "Tools/SMT/smt_monomorph.ML"
    1.31  use "Tools/SMT/smt_builtin.ML"
    1.32 +use "Tools/SMT/smt_datatypes.ML"
    1.33  use "Tools/SMT/smt_normalize.ML"
    1.34  use "Tools/SMT/smt_translate.ML"
    1.35  use "Tools/SMT/smt_solver.ML"
    1.36 @@ -380,13 +380,4 @@
    1.37  hide_const Pattern fun_app term_true term_false z3div z3mod
    1.38  hide_const (open) trigger pat nopat weight
    1.39  
    1.40 -
    1.41 -
    1.42 -subsection {* Selectors for datatypes *}
    1.43 -
    1.44 -setup {* Datatype_Selectors.setup *}
    1.45 -
    1.46 -declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
    1.47 -declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
    1.48 -
    1.49  end