src/ZF/Int_ZF.thy
changeset 61378 3e04c9ca001a
parent 60770 240563fbf41d
child 61395 4f8c2c4a0a8c
     1.1 --- a/src/ZF/Int_ZF.thy	Fri Oct 09 19:51:20 2015 +0200
     1.2 +++ b/src/ZF/Int_ZF.thy	Fri Oct 09 20:26:03 2015 +0200
     1.3 @@ -95,10 +95,6 @@
     1.4    zmult  (infixl "$\<times>" 70) and
     1.5    zle  (infixl "$\<le>" 50)  --\<open>less than or equals\<close>
     1.6  
     1.7 -notation (HTML output)
     1.8 -  zmult  (infixl "$\<times>" 70) and
     1.9 -  zle  (infixl "$\<le>" 50)
    1.10 -
    1.11  
    1.12  declare quotientE [elim!]
    1.13