# HG changeset patch
# User nipkow
# Date 1044957867 -3600
# Node ID 0832792725db31ac48ffd4a6fd61c893d21dfca1
# Parent  5402c2eaf393e4c9d7f72bf88c7dcacbe99680dd
*** empty log message ***

diff -r 5402c2eaf393 -r 0832792725db NEWS
--- a/NEWS	Mon Feb 10 15:57:46 2003 +0100
+++ b/NEWS	Tue Feb 11 11:04:27 2003 +0100
@@ -37,24 +37,25 @@
 
   - The simplifier trace now shows the names of the applied rewrite rules
 
-* Pure: new flag for triggering if the overall goal of a proof state should
-be printed (ML: Proof.show_main_goal).
-PG menu: Isabelle/Isar -> Settigs -> Show Main Goal
-
-* 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: new flag trace_unify_fail causes unification to print
+* Pure: New flag for triggering if the overall goal of a proof state should
+be printed:
+   PG menu: Isabelle/Isar -> Settigs -> Show Main Goal
+(ML: Proof.show_main_goal).
+
+* Pure: You can find all matching introduction rules for subgoal 1, i.e. all
+rules whose conclusion matches subgoal 1:
+      PG menu: Isabelle/Isar -> Show me -> matching rules
+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 they are printed).
+(ML: ProofGeneral.print_intros())
+
+* Pure: New flag trace_unify_fail causes unification to print
 diagnostic information (PG: in trace buffer) when it fails. This is
 useful for figuring out why single step proofs like rule, erule or
 assumption failed.
 
-* Pure: locale specifications now produce predicate definitions
+* 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,
 while "loc" is cumulative wrt. all included locale expressions; the