equal
deleted
inserted
replaced
40 |
40 |
41 * Pure: new flag trace_unify_fail causes unification to print |
41 * Pure: new flag trace_unify_fail causes unification to print |
42 diagnostic information (PG: in trace buffer) when it fails. This is |
42 diagnostic information (PG: in trace buffer) when it fails. This is |
43 useful for figuring out why single step proofs like rule, erule or |
43 useful for figuring out why single step proofs like rule, erule or |
44 assumption failed. |
44 assumption failed. |
|
45 |
|
46 * Pure: you can find all matching introduction rules for subgoal 1, |
|
47 i.e. all rules whose conclusion matches subgoal 1, by executing |
|
48 ML"ProofGeneral.print_intros()" |
|
49 The rules are ordered by how closely they match the subgoal. |
|
50 In particular, rules that solve a subgoal outright are displayed first |
|
51 (or rather last, the way it is printed). |
|
52 TODO: integration with PG |
45 |
53 |
46 * Pure: locale specifications now produce predicate definitions |
54 * Pure: locale specifications now produce predicate definitions |
47 according to the body of text (covering assumptions modulo local |
55 according to the body of text (covering assumptions modulo local |
48 definitions); predicate "loc_axioms" covers newly introduced text, |
56 definitions); predicate "loc_axioms" covers newly introduced text, |
49 while "loc" is cumulative wrt. all included locale expressions; the |
57 while "loc" is cumulative wrt. all included locale expressions; the |