src/HOL/HOL.thy
changeset 6340 7d5cbd5819a0
parent 6289 062aa156a300
child 6795 35f214e73668
     1.1 --- a/src/HOL/HOL.thy	Wed Mar 10 10:53:53 1999 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 10 10:55:12 1999 +0100
     1.3 @@ -140,10 +140,13 @@
     1.4    "*Ex"         :: [idts, bool] => bool             ("(3\\<exists>_./ _)" [0, 10] 10)
     1.5    "*Ex1"        :: [idts, bool] => bool             ("(3\\<exists>!_./ _)" [0, 10] 10)
     1.6  
     1.7 -
     1.8  syntax (xsymbols)
     1.9    "op -->"      :: [bool, bool] => bool             (infixr "\\<longrightarrow>" 25)
    1.10  
    1.11 +syntax (HTML output)
    1.12 +  Not           :: bool => bool                     ("\\<not> _" [40] 40)
    1.13 +
    1.14 +
    1.15  (** Rules and definitions **)
    1.16  
    1.17  local