--- a/src/HOLCF/Tr.thy Tue Mar 04 10:48:36 1997 +0100
+++ b/src/HOLCF/Tr.thy Tue Mar 04 10:58:29 1997 +0100
@@ -30,7 +30,7 @@
defs
TT_def "TT==Def True"
FF_def "FF==Def False"
- neg_def "neg == flift2 not"
+ neg_def "neg == flift2 Not"
ifte_def "Icifte == (LAM b t e.flift1(%b.if b then t else e)`b)"
andalso_def "trand == (LAM x y.If x then y else FF fi)"
orelse_def "tror == (LAM x y.If x then TT else y fi)"
--- a/src/HOLCF/ax_ops/holcflogic.ML Tue Mar 04 10:48:36 1997 +0100
+++ b/src/HOLCF/ax_ops/holcflogic.ML Tue Mar 04 10:58:29 1997 +0100
@@ -33,7 +33,7 @@
val False = Const("False",boolT);
val Imp = Const("op -->",boolT --> boolT --> boolT);
val And = Const("op &",boolT --> boolT --> boolT);
-val Not = Const("not",boolT --> boolT);
+val Not = Const("Not",boolT --> boolT);
fun mkNot A = Not $ A; (* negates, no Trueprop *)
--- a/src/HOLCF/domain/library.ML Tue Mar 04 10:48:36 1997 +0100
+++ b/src/HOLCF/domain/library.ML Tue Mar 04 10:58:29 1997 +0100
@@ -139,7 +139,7 @@
end;
fun mk_ex (x,P) = mk_exists (x,dummyT,P);
-fun mk_not P = Const("not" ,boolT --> boolT) $ P;
+fun mk_not P = Const("Not" ,boolT --> boolT) $ P;
end;
fun mk_All (x,P) = %%"all" $ mk_lam(x,P); (* meta universal quantification *)