| changeset 61378 | 3e04c9ca001a |
| parent 60770 | 240563fbf41d |
| child 61395 | 4f8c2c4a0a8c |
--- 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!]