equal
deleted
inserted
replaced
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 |
41 |
42 * Mixfix annotations may use "' " (single quote followed by space) to |
42 * Mixfix annotations may use "' " (single quote followed by space) to |
43 separate delimiters (as documented in the isar-ref manual), without |
43 separate delimiters (as documented in the isar-ref manual), without |
44 requiring an auxiliary empty block. |
44 requiring an auxiliary empty block. A literal single quote needs to be |
|
45 escaped properly: rare INCOMPATIBILITY. |
45 |
46 |
46 |
47 |
47 *** Isar *** |
48 *** Isar *** |
48 |
49 |
49 * The proof method combinator (subproofs m) applies the method |
50 * The proof method combinator (subproofs m) applies the method |