NEWS
changeset 71661 404624eb3a22
parent 71658 91340a6bf401
child 71686 be84312a2d53
equal deleted inserted replaced
71660:439410bf4519 71661:404624eb3a22
    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 
    35 
    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 
       
    39 * The inference kernel is now confined to one main module: structure
       
    40 Thm, without the former circular dependency on structure Axclass.
    38 
    41 
    39 
    42 
    40 *** Isar ***
    43 *** Isar ***
    41 
    44 
    42 * The proof method combinator (subproofs m) applies the method
    45 * The proof method combinator (subproofs m) applies the method