equal
deleted
inserted
replaced
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. A literal single quote needs to be |
44 requiring an auxiliary empty block. A literal single quote needs to be |
45 escaped properly: rare INCOMPATIBILITY. |
45 escaped properly. Minor INCOMPATIBILITY. |
46 |
46 |
47 |
47 |
48 *** Isar *** |
48 *** Isar *** |
49 |
49 |
50 * The proof method combinator (subproofs m) applies the method |
50 * The proof method combinator (subproofs m) applies the method |