# HG changeset patch
# User paulson
# Date 857552364 -3600
# Node ID 3490ef519a56238a2d4a4fe048f60a43b128d212
# Parent  27167b432e7a089726b32de475384a2448ddd532
Renamed constant "not" to "Not"

diff -r 27167b432e7a -r 3490ef519a56 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Mar 04 10:58:29 1997 +0100
+++ b/src/HOL/HOL.thy	Wed Mar 05 09:59:24 1997 +0100
@@ -30,7 +30,7 @@
   (* Constants *)
 
   Trueprop      :: bool => prop                     ("(_)" 5)
-  not           :: bool => bool                     ("~ _" [40] 40)
+  Not           :: bool => bool                     ("~ _" [40] 40)
   True, False   :: bool
   If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
   Inv           :: ('a => 'b) => ('b => 'a)
diff -r 27167b432e7a -r 3490ef519a56 src/HOL/ex/meson.ML
--- a/src/HOL/ex/meson.ML	Tue Mar 04 10:58:29 1997 +0100
+++ b/src/HOL/ex/meson.ML	Wed Mar 05 09:59:24 1997 +0100
@@ -200,7 +200,7 @@
 
 fun literals (Const("Trueprop",_) $ P) = literals P
   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
-  | literals (Const("not",_) $ P) = [(false,P)]
+  | literals (Const("Not",_) $ P) = [(false,P)]
   | literals P = [(true,P)];
 
 (*number of literals in a term*)