NEWS
changeset 71551 76ec3baeec9d
parent 71547 d350aabace23
child 71557 61ba52af28e3
child 71575 aff37005fd79
equal deleted inserted replaced
71550:f2b944898636 71551:76ec3baeec9d
    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