src/HOL/SMT.thy
changeset 40274 6486c610a549
parent 40162 7f58a9a843c2
child 40277 4e3a3461c1a6
     1.1 --- a/src/HOL/SMT.thy	Fri Oct 29 17:38:57 2010 +0200
     1.2 +++ b/src/HOL/SMT.thy	Fri Oct 29 18:17:04 2010 +0200
     1.3 @@ -49,6 +49,20 @@
     1.4  
     1.5  
     1.6  
     1.7 +subsection {* Distinctness *}
     1.8 +
     1.9 +text {*
    1.10 +As an abbreviation for a quadratic number of inequalities, SMT solvers
    1.11 +provide a built-in @{text distinct}.  To avoid confusion with the
    1.12 +already defined (and more general) @{term List.distinct}, a separate
    1.13 +constant is defined.
    1.14 +*}
    1.15 +
    1.16 +definition distinct :: "'a list \<Rightarrow> bool"
    1.17 +where "distinct xs = List.distinct xs"
    1.18 +
    1.19 +
    1.20 +
    1.21  subsection {* Higher-order encoding *}
    1.22  
    1.23  text {*
    1.24 @@ -314,7 +328,7 @@
    1.25  
    1.26  hide_type (open) pattern
    1.27  hide_const Pattern term_eq
    1.28 -hide_const (open) trigger pat nopat fun_app z3div z3mod
    1.29 +hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
    1.30  
    1.31  
    1.32