diff -r 517feb558c77 -r 3e04c9ca001a src/ZF/Int_ZF.thy
--- a/src/ZF/Int_ZF.thy	Fri Oct 09 19:51:20 2015 +0200
+++ b/src/ZF/Int_ZF.thy	Fri Oct 09 20:26:03 2015 +0200
@@ -95,10 +95,6 @@
   zmult  (infixl "$\<times>" 70) and
   zle  (infixl "$\<le>" 50)  --\<open>less than or equals\<close>
 
-notation (HTML output)
-  zmult  (infixl "$\<times>" 70) and
-  zle  (infixl "$\<le>" 50)
-
 
 declare quotientE [elim!]