src/HOL/SMT.thy
changeset 39483 9f0e5684f04b
parent 39298 5aefb5bc8a93
child 40162 7f58a9a843c2
     1.1 --- a/src/HOL/SMT.thy	Fri Sep 17 08:41:07 2010 +0200
     1.2 +++ b/src/HOL/SMT.thy	Fri Sep 17 10:52:35 2010 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  theory SMT
     1.5  imports List
     1.6  uses
     1.7 +  "Tools/Datatype/datatype_selectors.ML"
     1.8    ("Tools/SMT/smt_monomorph.ML")
     1.9    ("Tools/SMT/smt_normalize.ML")
    1.10    ("Tools/SMT/smt_translate.ML")
    1.11 @@ -323,4 +324,13 @@
    1.12  hide_const Pattern term_eq
    1.13  hide_const (open) trigger pat nopat fun_app z3div z3mod
    1.14  
    1.15 +
    1.16 +
    1.17 +subsection {* Selectors for datatypes *}
    1.18 +
    1.19 +setup {* Datatype_Selectors.setup *}
    1.20 +
    1.21 +declare [[ selector Pair 1 = fst, selector Pair 2 = snd ]]
    1.22 +declare [[ selector Cons 1 = hd, selector Cons 2 = tl ]]
    1.23 +
    1.24  end