Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
authorberghofe
Wed May 07 10:56:55 2008 +0200 (2008-05-07)
changeset 26804e2b1e6868c2f
parent 26803 0af0f674845d
child 26805 27941d7d9a11
Adapted functions mk_setT and dest_setT to encoding of sets as predicates.
src/HOL/hologic.ML
     1.1 --- a/src/HOL/hologic.ML	Wed May 07 10:56:52 2008 +0200
     1.2 +++ b/src/HOL/hologic.ML	Wed May 07 10:56:55 2008 +0200
     1.3 @@ -135,9 +135,9 @@
     1.4  val true_const =  Const ("True", boolT);
     1.5  val false_const = Const ("False", boolT);
     1.6  
     1.7 -fun mk_setT T = Type ("set", [T]);
     1.8 +fun mk_setT T = T --> boolT;
     1.9  
    1.10 -fun dest_setT (Type ("set", [T])) = T
    1.11 +fun dest_setT (Type ("fun", [T, Type ("bool", [])])) = T
    1.12    | dest_setT T = raise TYPE ("dest_setT: set type expected", [T], []);
    1.13  
    1.14