equal
deleted
inserted
replaced
61 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
61 * Removed exotic 'token_translation' command. INCOMPATIBILITY, use ML |
62 interface instead. |
62 interface instead. |
63 |
63 |
64 * There is a new syntactic category "float_const" for signed decimal |
64 * There is a new syntactic category "float_const" for signed decimal |
65 fractions (e.g. 123.45 or -123.45). |
65 fractions (e.g. 123.45 or -123.45). |
|
66 |
|
67 * New prover for coherent logic (see src/Tools/coherent.ML). |
66 |
68 |
67 |
69 |
68 *** Pure *** |
70 *** Pure *** |
69 |
71 |
70 * Class declaration: sc. "base sort" must not be given in import list |
72 * Class declaration: sc. "base sort" must not be given in import list |