NEWS
changeset 71446 91340a6bf401
parent 71438 22158ebde77f
child 71448 404624eb3a22
equal deleted inserted replaced
71445:e596ea18bf3e 71446:91340a6bf401
    30 covering the full graph of transitive dependencies.
    30 covering the full graph of transitive dependencies.
    31 
    31 
    32 * Command 'thm_deps' prints immediate theorem dependencies of the given
    32 * Command 'thm_deps' prints immediate theorem dependencies of the given
    33 facts. The former graph visualization has been discontinued, because it
    33 facts. The former graph visualization has been discontinued, because it
    34 was hardly usable.
    34 was hardly usable.
       
    35 
       
    36 * Refined treatment of proof terms, including type-class proofs for
       
    37 minor object-logics (FOL, FOLP, Sequents).
    35 
    38 
    36 
    39 
    37 *** Isar ***
    40 *** Isar ***
    38 
    41 
    39 * The proof method combinator (subproofs m) applies the method
    42 * The proof method combinator (subproofs m) applies the method