src/HOL/SMT.thy
changeset 41281 679118e35378
parent 41280 a7de9d36f4f2
child 41328 6792a5c92a58
     1.1 --- a/src/HOL/SMT.thy	Sun Dec 19 17:55:56 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Sun Dec 19 18:54:29 2010 +0100
     1.3 @@ -113,12 +113,14 @@
     1.4  uninterpreted constants (those not built-in in the target solver)
     1.5  are treated as function symbols in the first-order sense.  Their
     1.6  occurrences as head symbols in atoms (i.e., as predicate symbols) are
     1.7 -turned into terms by equating such atoms with @{term True}.
     1.8 -Whenever the boolean type occurs in first-order terms, it is replaced
     1.9 -by the following type.
    1.10 +turned into terms by logically equating such atoms with @{term True}.
    1.11 +For technical reasons, @{term True} and @{term False} occurring inside
    1.12 +terms are replaced by the following constants.
    1.13  *}
    1.14  
    1.15 -typedecl term_bool
    1.16 +definition term_true where "term_true = True"
    1.17 +definition term_false where "term_false = False"
    1.18 +
    1.19  
    1.20  
    1.21  
    1.22 @@ -374,9 +376,8 @@
    1.23  
    1.24  
    1.25  
    1.26 -hide_type term_bool
    1.27  hide_type (open) pattern
    1.28 -hide_const Pattern fun_app z3div z3mod
    1.29 +hide_const Pattern fun_app term_true term_false z3div z3mod
    1.30  hide_const (open) trigger pat nopat weight
    1.31  
    1.32