src/ZF/Integ/Int.thy
changeset 14565 c6dc17aab88a
parent 14511 73493236e97f
child 15182 5cea84e10f3e
     1.1 --- a/src/ZF/Integ/Int.thy	Wed Apr 14 13:28:46 2004 +0200
     1.2 +++ b/src/ZF/Integ/Int.thy	Wed Apr 14 14:13:05 2004 +0200
     1.3 @@ -82,6 +82,7 @@
     1.4  
     1.5  syntax (HTML output)
     1.6    zmult :: "[i,i]=>i"          (infixl "$\<times>" 70)
     1.7 +  zle   :: "[i,i]=>o"          (infixl "$\<le>" 50)
     1.8  
     1.9  
    1.10  declare quotientE [elim!]