# HG changeset patch
# User nipkow
# Date 1034595317 -7200
# Node ID 610cedff553889ebb860fbae12abebf69b9dc8a1
# Parent  7f6f0ffc45c3c798304d88732658788e68be45d4
*** empty log message ***

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