src/HOL/SMT.thy
changeset 40681 872b08416fb4
parent 40664 e023788a91a1
child 40806 59d96f777da3
     1.1 --- a/src/HOL/SMT.thy	Wed Nov 24 08:51:48 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Wed Nov 24 10:39:58 2010 +0100
     1.3 @@ -81,20 +81,6 @@
     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 @@ -369,7 +355,7 @@
    1.25  
    1.26  hide_type (open) pattern
    1.27  hide_const Pattern term_eq
    1.28 -hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod
    1.29 +hide_const (open) trigger pat nopat weight fun_app z3div z3mod
    1.30  
    1.31  
    1.32