src/ZF/int_arith.ML

--- a/src/ZF/int_arith.ML	Sat Oct 10 22:14:44 2015 +0200
+++ b/src/ZF/int_arith.ML	Sat Oct 10 22:19:06 2015 +0200
@@ -221,9 +221,9 @@
     proc = K LessCancelNumerals.proc, identifier = []},
   Simplifier.make_simproc @{context} "intle_cancel_numerals"
    {lhss =
-     [@{term "l $+ m $<= n"}, @{term "l $<= m $+ n"},
-      @{term "l $- m $<= n"}, @{term "l $<= m $- n"},
-      @{term "l $* m $<= n"}, @{term "l $<= m $* n"}],
+     [@{term "l $+ m $\<le> n"}, @{term "l $\<le> m $+ n"},
+      @{term "l $- m $\<le> n"}, @{term "l $\<le> m $- n"},
+      @{term "l $* m $\<le> n"}, @{term "l $\<le> m $* n"}],
     proc = K LeCancelNumerals.proc, identifier = []}];