equal
deleted
inserted
replaced
345 INCOMPATIBILITY. |
345 INCOMPATIBILITY. |
346 |
346 |
347 |
347 |
348 *** ML *** |
348 *** ML *** |
349 |
349 |
350 * Ad-hoc overloading for standard operations on type Rat.rat: + - * / = |
350 * Structure Rat for rational numbers is now an integral part of |
351 < <= > >= <> ~ abs. INCOMPATIBILITY, need to use + instead of +/ etc. |
351 Isabelle/ML, with special notation @int/nat for numerals (an |
|
352 abbreviation for antiquotation @{Pure.rat int/nat}) and ML pretty |
|
353 printing. Standard operations on type Rat.rat are provided via ad-hoc |
|
354 overloading of + - * / = < <= > >= <> ~ abs. INCOMPATIBILITY, need to |
|
355 use + instead of +/ etc. Moreover, exception Rat.DIVZERO has been |
|
356 superseded by General.Div. |
352 |
357 |
353 * The ML function "ML" provides easy access to run-time compilation. |
358 * The ML function "ML" provides easy access to run-time compilation. |
354 This is particularly useful for conditional compilation, without |
359 This is particularly useful for conditional compilation, without |
355 requiring separate files. |
360 requiring separate files. |
356 |
361 |