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