Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Renamed constant "not" to "Not"
authorpaulson
Wed, 05 Mar 1997 09:59:24 +0100
changeset 2720 3490ef519a56
parent 2719 27167b432e7a
child 2721 f08042e18c7d
Renamed constant "not" to "Not"
src/HOL/HOL.thy file | annotate | diff | comparison | revisions
src/HOL/ex/meson.ML file | annotate | diff | comparison | revisions 
--- 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)
--- 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*)
isabelle