1.1 --- a/NEWS	Mon Mar 17 18:38:50 2003 +0100
     1.2 +++ b/NEWS	Tue Mar 18 17:54:27 2003 +0100
     1.3 @@ -46,8 +46,8 @@
     1.4  
     1.5    - Accepts free variables as head terms in congruence rules.  Useful in Isar.
     1.6  
     1.7 -* Pure: New flag for triggering if the overall goal of a proof state should
     1.8 -be printed:
     1.9 +* Pure: The main goal of the proof state is no longer shown by default, only
    1.10 +the subgoals. This behaviour is controlled by a new flag.
    1.11     PG menu: Isabelle/Isar -> Settings -> Show Main Goal
    1.12  (ML: Proof.show_main_goal).
    1.13