added not;
authorwenzelm
Tue Sep 05 18:45:51 2000 +0200 (2000-09-05 ago)
changeset 9850bee6eb4b6a42
parent 9849 71ad08ad2cf0
child 9851 e22db9397e17
added not;
src/FOL/fologic.ML
     1.1 --- a/src/FOL/fologic.ML	Tue Sep 05 18:45:09 2000 +0200
     1.2 +++ b/src/FOL/fologic.ML	Tue Sep 05 18:45:51 2000 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val mk_Trueprop	: term -> term
     1.5    val atomic_Trueprop	: string -> term
     1.6    val dest_Trueprop	: term -> term
     1.7 +  val not		: term
     1.8    val conj		: term
     1.9    val disj		: term
    1.10    val imp		: term
    1.11 @@ -50,10 +51,11 @@
    1.12  
    1.13  (** Logical constants **)
    1.14  
    1.15 -val conj = Const("op &", [oT,oT]--->oT)
    1.16 -and disj = Const("op |", [oT,oT]--->oT)
    1.17 -and imp = Const("op -->", [oT,oT]--->oT)
    1.18 -and iff = Const("op <->", [oT,oT]--->oT);
    1.19 +val not = Const ("Not", oT --> oT);
    1.20 +val conj = Const("op &", [oT,oT]--->oT);
    1.21 +val disj = Const("op |", [oT,oT]--->oT);
    1.22 +val imp = Const("op -->", [oT,oT]--->oT)
    1.23 +val iff = Const("op <->", [oT,oT]--->oT);
    1.24  
    1.25  fun mk_conj (t1, t2) = conj $ t1 $ t2
    1.26  and mk_disj (t1, t2) = disj $ t1 $ t2