# HG changeset patch
# User paulson
# Date 857469509 -3600
# Node ID 27167b432e7a089726b32de475384a2448ddd532
# Parent  460fd0f8d478a8f886c1eaa07c5135d6e8aced4e
Renamed constant "not" to "Not"

diff -r 460fd0f8d478 -r 27167b432e7a src/HOLCF/Tr.thy
--- 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)"
diff -r 460fd0f8d478 -r 27167b432e7a src/HOLCF/ax_ops/holcflogic.ML
--- 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 *)
 
diff -r 460fd0f8d478 -r 27167b432e7a src/HOLCF/domain/library.ML
--- 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 *)