equal
deleted
inserted
replaced
220 |
220 |
221 *** HOL *** |
221 *** HOL *** |
222 |
222 |
223 * New predicate "strict_mono" classifies strict functions on partial orders. |
223 * New predicate "strict_mono" classifies strict functions on partial orders. |
224 With strict functions on linear orders, reasoning about (in)equalities is |
224 With strict functions on linear orders, reasoning about (in)equalities is |
225 facilitated by theorems "strict_mono_eq", "strict_mono_eq" and "strict_mono_eq". |
225 facilitated by theorems "strict_mono_eq", "strict_mono_less_eq" and "strict_mono_less". |
226 |
226 |
227 * Auxiliary class "itself" has disappeared -- classes without any parameter |
227 * Auxiliary class "itself" has disappeared -- classes without any parameter |
228 are treated as expected by the 'class' command. |
228 are treated as expected by the 'class' command. |
229 |
229 |
230 * Leibnitz's Series for Pi and the arcus tangens and logarithm series. |
230 * Leibnitz's Series for Pi and the arcus tangens and logarithm series. |