equal
deleted
inserted
replaced
36 * Refined treatment of proof terms, including type-class proofs for |
36 * Refined treatment of proof terms, including type-class proofs for |
37 minor object-logics (FOL, FOLP, Sequents). |
37 minor object-logics (FOL, FOLP, Sequents). |
38 |
38 |
39 * The inference kernel is now confined to one main module: structure |
39 * The inference kernel is now confined to one main module: structure |
40 Thm, without the former circular dependency on structure Axclass. |
40 Thm, without the former circular dependency on structure Axclass. |
|
41 |
|
42 * Mixfix annotations may use "' " (single quote followed by space) to |
|
43 separate delimiters (as documented in the isar-ref manual), without |
|
44 requiring an auxiliary empty block. |
41 |
45 |
42 |
46 |
43 *** Isar *** |
47 *** Isar *** |
44 |
48 |
45 * The proof method combinator (subproofs m) applies the method |
49 * The proof method combinator (subproofs m) applies the method |