--- a/NEWS Thu Mar 16 20:19:25 2006 +0100
+++ b/NEWS Fri Mar 17 09:34:23 2006 +0100
@@ -346,19 +346,21 @@
25 like -->); output depends on the "iff" print_mode, the default is
"A = B" (with priority 50).
-* Renamed some (legacy-named) constants in HOL.thy:
+* Renamed some (legacy-named) constants in HOL.thy and Orderings.thy:
op + ~> HOL.plus
op - ~> HOL.minus
uminus ~> HOL.uminus
op * ~> HOL.times
+ op < ~> Orderings.less
+ op <= ~> Orderings.less_eq
Adaptions may be required in the following cases:
-a) User-defined constants using any of the names "plus", "minus", or "times"
-The standard syntax translations for "+", "-" and "*" may go wrong.
+a) User-defined constants using any of the names "plus", "minus", "times", "less"
+or "less_eq". The standard syntax translations for "+", "-" and "*" may go wrong.
INCOMPATIBILITY: use more specific names.
-b) Variables named "plus", "minus", or "times"
+b) Variables named "plus", "minus", "times", "less", "less_eq"
INCOMPATIBILITY: use more specific names.
c) Commutative equations theorems (e. g. "a + b = b + a")