1.1 --- a/NEWS	Mon Oct 14 11:32:00 2002 +0200
     1.2 +++ b/NEWS	Mon Oct 14 13:35:17 2002 +0200
     1.3 @@ -43,6 +43,14 @@
     1.4  useful for figuring out why single step proofs like rule, erule or
     1.5  assumption failed.
     1.6  
     1.7 +* Pure: you can find all matching introduction rules for subgoal 1,
     1.8 +  i.e. all rules whose conclusion matches subgoal 1, by executing
     1.9 +  ML"ProofGeneral.print_intros()"
    1.10 +  The rules are ordered by how closely they match the subgoal.
    1.11 +  In particular, rules that solve a subgoal outright are displayed first
    1.12 +  (or rather last, the way it is printed).
    1.13 +  TODO: integration with PG
    1.14 +
    1.15  * Pure: locale specifications now produce predicate definitions
    1.16  according to the body of text (covering assumptions modulo local
    1.17  definitions); predicate "loc_axioms" covers newly introduced text,