added Not;
authorwenzelm
Mon Mar 13 13:17:52 2000 +0100 (2000-03-13)
changeset 8429515fa7533354
parent 8428 be4c8a57cf7e
child 8430 dbd897e0d804
added Not;
src/HOL/hologic.ML
     1.1 --- a/src/HOL/hologic.ML	Mon Mar 13 13:16:57 2000 +0100
     1.2 +++ b/src/HOL/hologic.ML	Mon Mar 13 13:17:52 2000 +0100
     1.3 @@ -21,6 +21,7 @@
     1.4    val conj: term
     1.5    val disj: term
     1.6    val imp: term
     1.7 +  val Not: term
     1.8    val mk_conj: term * term -> term
     1.9    val mk_disj: term * term -> term
    1.10    val mk_imp: term * term -> term
    1.11 @@ -106,7 +107,8 @@
    1.12  
    1.13  val conj = Const ("op &", [boolT, boolT] ---> boolT)
    1.14  and disj = Const ("op |", [boolT, boolT] ---> boolT)
    1.15 -and imp = Const ("op -->", [boolT, boolT] ---> boolT);
    1.16 +and imp = Const ("op -->", [boolT, boolT] ---> boolT)
    1.17 +and Not = Const ("Not", boolT --> boolT);
    1.18  
    1.19  fun mk_conj (t1, t2) = conj $ t1 $ t2
    1.20  and mk_disj (t1, t2) = disj $ t1 $ t2