| changeset 6340 | 7d5cbd5819a0 | 
| parent 6289 | 062aa156a300 | 
| child 6795 | 35f214e73668 | 
--- a/src/HOL/HOL.thy Wed Mar 10 10:53:53 1999 +0100 +++ b/src/HOL/HOL.thy Wed Mar 10 10:55:12 1999 +0100 @@ -140,10 +140,13 @@ "*Ex" :: [idts, bool] => bool ("(3\\<exists>_./ _)" [0, 10] 10) "*Ex1" :: [idts, bool] => bool ("(3\\<exists>!_./ _)" [0, 10] 10) - syntax (xsymbols) "op -->" :: [bool, bool] => bool (infixr "\\<longrightarrow>" 25) +syntax (HTML output) + Not :: bool => bool ("\\<not> _" [40] 40) + + (** Rules and definitions **) local