# HG changeset patch
# User nipkow
# Date 1048006467 -3600
# Node ID 01b516b64233d56a4b87e1f3929fdbf2066bed23
# Parent  1fdecd15437fd7a3ae24c901322a891b2ecb31ec
*** empty log message ***

diff -r 1fdecd15437f -r 01b516b64233 NEWS
--- a/NEWS	Mon Mar 17 18:38:50 2003 +0100
+++ b/NEWS	Tue Mar 18 17:54:27 2003 +0100
@@ -46,8 +46,8 @@
 
   - Accepts free variables as head terms in congruence rules.  Useful in Isar.
 
-* Pure: New flag for triggering if the overall goal of a proof state should
-be printed:
+* Pure: The main goal of the proof state is no longer shown by default, only
+the subgoals. This behaviour is controlled by a new flag.
    PG menu: Isabelle/Isar -> Settings -> Show Main Goal
 (ML: Proof.show_main_goal).
 
diff -r 1fdecd15437f -r 01b516b64233 doc-src/TutorialI/ToyList/ToyList.thy
--- a/doc-src/TutorialI/ToyList/ToyList.thy	Mon Mar 17 18:38:50 2003 +0100
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Mar 18 17:54:27 2003 +0100
@@ -144,23 +144,21 @@
 The name and the simplification attribute are optional.
 Isabelle's response is to print the initial proof state consisting
 of some header information (like how many subgoals there are) followed by
-@{goals[display,indent=0]}
+@{subgoals[display,indent=0]}
 For compactness reasons we omit the header in this tutorial.
 Until we have finished a proof, the \rmindex{proof state} proper
 always looks like this:
 \begin{isabelle}
-$G$\isanewline
 ~1.~$G\sb{1}$\isanewline
 ~~\vdots~~\isanewline
 ~$n$.~$G\sb{n}$
 \end{isabelle}
-where $G$
-is the overall goal that we are trying to prove, and the numbered lines
-contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
-establish $G$.\index{subgoals}
-Initially there is only one subgoal, which is
-identical with the overall goal.  Normally $G$ is constant and only serves as
-a reminder. Hence we rarely show it in this tutorial.
+The numbered lines contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$
+that we need to prove to establish the main goal.\index{subgoals}
+Initially there is only one subgoal, which is identical with the
+main goal. (If you always want to see the main goal as well,
+set the flag \isa{Proof.show_main_goal}\index{*show_main_goal (flag)}
+--- this flag used to be set by default.)
 
 Let us now get back to @{prop"rev(rev xs) = xs"}. Properties of recursively
 defined functions are best established by induction. In this case there is