# 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*)