Renamed constant "not" to "Not"
authorpaulson
Wed Mar 05 09:59:24 1997 +0100 (1997-03-05)
changeset 27203490ef519a56
parent 2719 27167b432e7a
child 2721 f08042e18c7d
Renamed constant "not" to "Not"
src/HOL/HOL.thy
src/HOL/ex/meson.ML
     1.1 --- a/src/HOL/HOL.thy	Tue Mar 04 10:58:29 1997 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 05 09:59:24 1997 +0100
     1.3 @@ -30,7 +30,7 @@
     1.4    (* Constants *)
     1.5  
     1.6    Trueprop      :: bool => prop                     ("(_)" 5)
     1.7 -  not           :: bool => bool                     ("~ _" [40] 40)
     1.8 +  Not           :: bool => bool                     ("~ _" [40] 40)
     1.9    True, False   :: bool
    1.10    If            :: [bool, 'a, 'a] => 'a   ("(if (_)/ then (_)/ else (_))" 10)
    1.11    Inv           :: ('a => 'b) => ('b => 'a)
     2.1 --- a/src/HOL/ex/meson.ML	Tue Mar 04 10:58:29 1997 +0100
     2.2 +++ b/src/HOL/ex/meson.ML	Wed Mar 05 09:59:24 1997 +0100
     2.3 @@ -200,7 +200,7 @@
     2.4  
     2.5  fun literals (Const("Trueprop",_) $ P) = literals P
     2.6    | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
     2.7 -  | literals (Const("not",_) $ P) = [(false,P)]
     2.8 +  | literals (Const("Not",_) $ P) = [(false,P)]
     2.9    | literals P = [(true,P)];
    2.10  
    2.11  (*number of literals in a term*)