src/HOL/HOL.thy
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