*** empty log message ***
Tue, 18 Mar 2003 17:54:27 +0100
changeset 13868 01b516b64233
parent 13867 1fdecd15437f
child 13869 18112403c809
*** empty log message ***
--- 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).
--- 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
 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:
-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