--- a/src/ZF/Arith.thy Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/Arith.thy Fri Oct 09 20:26:03 2015 +0200
@@ -75,9 +75,6 @@
notation (xsymbols)
mult (infixr "#\<times>" 70)
-notation (HTML output)
- mult (infixr "#\<times>" 70)
-
declare rec_type [simp]
nat_0_le [simp]