equal
deleted
inserted
replaced
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 |