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  

     2.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Mon Mar 17 18:38:50 2003 +0100
     2.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Mar 18 17:54:27 2003 +0100
     2.3 @@ -144,23 +144,21 @@
     2.4  The name and the simplification attribute are optional.
     2.5  Isabelle's response is to print the initial proof state consisting
     2.6  of some header information (like how many subgoals there are) followed by
     2.7 -@{goals[display,indent=0]}
     2.8 +@{subgoals[display,indent=0]}
     2.9  For compactness reasons we omit the header in this tutorial.
    2.10  Until we have finished a proof, the \rmindex{proof state} proper
    2.11  always looks like this:
    2.12  \begin{isabelle}
    2.13 -$G$\isanewline
    2.14  ~1.~$G\sb{1}$\isanewline
    2.15  ~~\vdots~~\isanewline
    2.16  ~$n$.~$G\sb{n}$
    2.17  \end{isabelle}
    2.18 -where $G$
    2.19 -is the overall goal that we are trying to prove, and the numbered lines
    2.20 -contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
    2.21 -establish $G$.\index{subgoals}
    2.22 -Initially there is only one subgoal, which is
    2.23 -identical with the overall goal.  Normally $G$ is constant and only serves as
    2.24 -a reminder. Hence we rarely show it in this tutorial.
    2.25 +The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$
    2.26 +that we need to prove to establish the main goal.\index{subgoals}
    2.27 +Initially there is only one subgoal, which is identical with the
    2.28 +main goal. (If you always want to see the main goal as well,
    2.29 +set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}
    2.30 +--- this flag used to be set by default.)
    2.31  
    2.32  Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
    2.33  defined functions are best established by induction. In this case there is