# HG changeset patch
# User wenzelm
# Date 921059712 -3600
# Node ID 7d5cbd5819a09aa38ae51ad3653b40c523e1d29c
# Parent  b995ab76811795ead6f13bc8e01e948da14baf74
HTML output;

diff -r b995ab768117 -r 7d5cbd5819a0 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Wed Mar 10 10:53:53 1999 +0100
+++ b/src/FOL/IFOL.thy	Wed Mar 10 10:55:12 1999 +0100
@@ -67,6 +67,10 @@
   "op -->"      :: [o, o] => o                  (infixr "\\<longrightarrow>" 25)
   "op <->"      :: [o, o] => o                  (infixr "\\<longleftrightarrow>" 25)
 
+syntax (HTML output)
+  Not           :: o => o                       ("\\<not> _" [40] 40)
+
+
 local
 
 rules
diff -r b995ab768117 -r 7d5cbd5819a0 src/HOL/HOL.thy
--- 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
diff -r b995ab768117 -r 7d5cbd5819a0 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Wed Mar 10 10:53:53 1999 +0100
+++ b/src/HOL/Prod.thy	Wed Mar 10 10:55:12 1999 +0100
@@ -27,6 +27,9 @@
 syntax (symbols)
   "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
 
+syntax (HTML output)
+  "*"           :: [type, type] => type         ("(_ \\<times>/ _)" [21, 20] 20)
+
 
 (* abstract constants and syntax *)
 
diff -r b995ab768117 -r 7d5cbd5819a0 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Wed Mar 10 10:53:53 1999 +0100
+++ b/src/HOL/TLA/Intensional.thy	Wed Mar 10 10:55:12 1999 +0100
@@ -161,6 +161,9 @@
   "_liftMem"    :: [lift, lift] => lift                ("(_/ \\<in> _)" [50, 51] 50)
   "_liftNotMem" :: [lift, lift] => lift                ("(_/ \\<notin> _)" [50, 51] 50)
 
+syntax (HTML output)
+  "_liftNot"    :: lift => lift                        ("\\<not> _" [40] 40)
+
 rules
   Valid_def   "|- A    ==  ALL w. w |= A"
 
@@ -173,5 +176,3 @@
   unl_Rex     "w |= ? x. A x  ==  ? x. (w |= A x)"
   unl_Rex1    "w |= ?! x. A x  ==  ?! x. (w |= A x)"
 end
-
-ML
diff -r b995ab768117 -r 7d5cbd5819a0 src/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Mar 10 10:53:53 1999 +0100
+++ b/src/HOLCF/IOA/meta_theory/Pred.thy	Wed Mar 10 10:55:12 1999 +0100
@@ -41,6 +41,9 @@
 syntax (symbols)
   "satisfies"  ::"'a => 'a predicate => bool"    ("_ \\<Turnstile> _" [100,9] 8)
 
+syntax (HTML output)
+  "NOT"    ::"'a predicate => 'a predicate" ("\\<not> _" [40] 40)
+
 
 defs
 
diff -r b995ab768117 -r 7d5cbd5819a0 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Wed Mar 10 10:53:53 1999 +0100
+++ b/src/ZF/ZF.thy	Wed Mar 10 10:55:12 1999 +0100
@@ -164,6 +164,9 @@
   "@pattern"  :: patterns => pttrn         ("\\<langle>_\\<rangle>")
 *)
 
+syntax (HTML output)
+  "op *"      :: [i, i] => i               (infixr "\\<times>" 80)
+
 
 defs