--- 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