NEWS
 changeset 13815 0832792725db parent 13781 ecb2df44253e child 13824 e4d8dea6dfc2
```     1.1 --- a/NEWS	Mon Feb 10 15:57:46 2003 +0100
1.2 +++ b/NEWS	Tue Feb 11 11:04:27 2003 +0100
1.3 @@ -37,24 +37,25 @@
1.4
1.5    - The simplifier trace now shows the names of the applied rewrite rules
1.6
1.7 -* Pure: new flag for triggering if the overall goal of a proof state should
1.8 -be printed (ML: Proof.show_main_goal).
1.9 -PG menu: Isabelle/Isar -> Settigs -> Show Main Goal
1.10 -
1.11 -* Pure: you can find all matching introduction rules for subgoal 1,
1.12 -  i.e. all rules whose conclusion matches subgoal 1, by executing
1.13 -  ML"ProofGeneral.print_intros()"
1.14 -  The rules are ordered by how closely they match the subgoal.
1.15 -  In particular, rules that solve a subgoal outright are displayed first
1.16 -  (or rather last, the way it is printed).
1.17 -  TODO: integration with PG
1.18 -
1.19 -* Pure: new flag trace_unify_fail causes unification to print
1.20 +* Pure: New flag for triggering if the overall goal of a proof state should
1.21 +be printed:
1.22 +   PG menu: Isabelle/Isar -> Settigs -> Show Main Goal
1.23 +(ML: Proof.show_main_goal).
1.24 +
1.25 +* Pure: You can find all matching introduction rules for subgoal 1, i.e. all
1.26 +rules whose conclusion matches subgoal 1:
1.27 +      PG menu: Isabelle/Isar -> Show me -> matching rules
1.28 +The rules are ordered by how closely they match the subgoal.
1.29 +In particular, rules that solve a subgoal outright are displayed first
1.30 +(or rather last, the way they are printed).
1.31 +(ML: ProofGeneral.print_intros())
1.32 +
1.33 +* Pure: New flag trace_unify_fail causes unification to print
1.34  diagnostic information (PG: in trace buffer) when it fails. This is
1.35  useful for figuring out why single step proofs like rule, erule or
1.36  assumption failed.
1.37
1.38 -* Pure: locale specifications now produce predicate definitions
1.39 +* Pure: Locale specifications now produce predicate definitions
1.40  according to the body of text (covering assumptions modulo local
1.41  definitions); predicate "loc_axioms" covers newly introduced text,
1.42  while "loc" is cumulative wrt. all included locale expressions; the
```