src/HOL/hologic.ML
changeset 16835 2e7d7ec7a268
parent 15965 f422f8283491
child 16971 968adbfbf93b
     1.1 --- a/src/HOL/hologic.ML	Thu Jul 14 19:28:16 2005 +0200
     1.2 +++ b/src/HOL/hologic.ML	Thu Jul 14 19:28:17 2005 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    val boolT: typ
     1.5    val false_const: term
     1.6    val true_const: term
     1.7 -  val not_const: term
     1.8    val mk_setT: typ -> typ
     1.9    val dest_setT: typ -> typ
    1.10    val Trueprop: term
    1.11 @@ -27,6 +26,7 @@
    1.12    val mk_conj: term * term -> term
    1.13    val mk_disj: term * term -> term
    1.14    val mk_imp: term * term -> term
    1.15 +  val mk_not: term -> term
    1.16    val dest_conj: term -> term list
    1.17    val dest_disj: term -> term list
    1.18    val dest_imp: term -> term * term
    1.19 @@ -108,7 +108,6 @@
    1.20  
    1.21  val true_const =  Const ("True", boolT);
    1.22  val false_const = Const ("False", boolT);
    1.23 -val not_const = Const ("Not", boolT --> boolT);
    1.24  
    1.25  fun mk_setT T = Type ("set", [T]);
    1.26  
    1.27 @@ -133,7 +132,8 @@
    1.28  
    1.29  fun mk_conj (t1, t2) = conj $ t1 $ t2
    1.30  and mk_disj (t1, t2) = disj $ t1 $ t2
    1.31 -and mk_imp (t1, t2) = imp $ t1 $ t2;
    1.32 +and mk_imp (t1, t2) = imp $ t1 $ t2
    1.33 +and mk_not t = Not $ t;
    1.34  
    1.35  fun dest_conj (Const ("op &", _) $ t $ t') = t :: dest_conj t'
    1.36    | dest_conj t = [t];