# HG changeset patch
# User nipkow
# Date 1118421407 -7200
# Node ID af7239e3054d4f98c22c6d8d5dac6616fb0634ac
# Parent  2e2a506553a3b701c2a4f6c313bf7c3fdc0b2241
tuning

diff -r 2e2a506553a3 -r af7239e3054d doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Jun 10 17:59:12 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Jun 10 18:36:47 2005 +0200
@@ -441,13 +441,9 @@
 \begin{isamarkuptext}%
 \indexbold{tracing the simplifier}
 Using the simplifier effectively may take a bit of experimentation.  Set the
-\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} 
-to get a better idea of what is going
-on:%
+Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{ML}\ {\isachardoublequote}set\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
-\isamarkupfalse%
 \isacommand{lemma}\ {\isachardoublequote}rev\ {\isacharbrackleft}a{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline
 \isamarkupfalse%
 \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse%
@@ -455,40 +451,50 @@
 %
 \begin{isamarkuptext}%
 \noindent
-produces the trace
+produces the following trace in Proof General's \textsf{Trace} buffer:
 
 \begin{ttbox}\makeatother
-Applying instance of rewrite rule:
-rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
-Rewriting:
-rev [a] == rev [] @ [a]
-Applying instance of rewrite rule:
-rev [] == []
-Rewriting:
-rev [] == []
-Applying instance of rewrite rule:
-[] @ ?y == ?y
-Rewriting:
-[] @ [a] == [a]
-Applying instance of rewrite rule:
-?x3 \# ?t3 = ?t3 == False
-Rewriting:
-[a] = [] == False
+[0]Applying instance of rewrite rule "List.rev.simps_2":
+rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
+
+[0]Rewriting:
+rev [a] \(\equiv\) rev [] @ [a]
+
+[0]Applying instance of rewrite rule "List.rev.simps_1":
+rev [] \(\equiv\) []
+
+[0]Rewriting:
+rev [] \(\equiv\) []
+
+[0]Applying instance of rewrite rule "List.op @.append_Nil":
+[] @ ?y \(\equiv\) ?y
+
+[0]Rewriting:
+[] @ [a] \(\equiv\) [a]
+
+[0]Applying instance of rewrite rule
+?x2 # ?t1 = ?t1 \(\equiv\) False
+
+[0]Rewriting:
+[a] = [] \(\equiv\) False
 \end{ttbox}
+The trace lists each rule being applied, both in its general form and
+the instance being used. The \texttt{[}$i$\texttt{]} in front (where
+above $i$ is always \texttt{0}) indicates that we are inside the $i$th
+recursive invocation of the simplifier. Each attempt to apply a
+conditional rule shows the rule followed by the trace of the
+(recursive!) simplification of the conditions, the latter prefixed by
+\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
+Another source of recursive invocations of the simplifier are
+proofs of arithmetic formulae.
 
-The trace lists each rule being applied, both in its general form and the 
-instance being used.  For conditional rules, the trace lists the rule
-it is trying to rewrite and gives the result of attempting to prove
-each of the rule's conditions.  Many other hints about the simplifier's
-actions will appear.
+Many other hints about the simplifier's actions may appear.
 
-In more complicated cases, the trace can be quite lengthy.  Invocations of the
-simplifier are often nested, for instance when solving conditions of rewrite
-rules.  Thus it is advisable to reset it:%
+In more complicated cases, the trace can be very lengthy.  Thus it is
+advisable to reset the \textsf{Trace Simplifier} flag after having
+obtained the desired trace.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{ML}\ {\isachardoublequote}reset\ trace{\isacharunderscore}simp{\isachardoublequote}\isanewline
-\isamarkupfalse%
 \isamarkupfalse%
 \end{isabellebody}%
 %%% Local Variables:
diff -r 2e2a506553a3 -r af7239e3054d doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Fri Jun 10 17:59:12 2005 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Fri Jun 10 18:36:47 2005 +0200
@@ -367,50 +367,56 @@
 subsection{*Tracing*}
 text{*\indexbold{tracing the simplifier}
 Using the simplifier effectively may take a bit of experimentation.  Set the
-\isa{trace_simp}\index{*trace_simp (flag)} flag\index{flags} 
-to get a better idea of what is going
-on:
+Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Trace Simplifier} to get a better idea of what is going on:
 *}
 
-ML "set trace_simp"
 lemma "rev [a] = []"
 apply(simp)
 (*<*)oops(*>*)
 
 text{*\noindent
-produces the trace
+produces the following trace in Proof General's \textsf{Trace} buffer:
 
 \begin{ttbox}\makeatother
-Applying instance of rewrite rule:
-rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
-Rewriting:
-rev [a] == rev [] @ [a]
-Applying instance of rewrite rule:
-rev [] == []
-Rewriting:
-rev [] == []
-Applying instance of rewrite rule:
-[] @ ?y == ?y
-Rewriting:
-[] @ [a] == [a]
-Applying instance of rewrite rule:
-?x3 \# ?t3 = ?t3 == False
-Rewriting:
-[a] = [] == False
+[0]Applying instance of rewrite rule "List.rev.simps_2":
+rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
+
+[0]Rewriting:
+rev [a] \(\equiv\) rev [] @ [a]
+
+[0]Applying instance of rewrite rule "List.rev.simps_1":
+rev [] \(\equiv\) []
+
+[0]Rewriting:
+rev [] \(\equiv\) []
+
+[0]Applying instance of rewrite rule "List.op @.append_Nil":
+[] @ ?y \(\equiv\) ?y
+
+[0]Rewriting:
+[] @ [a] \(\equiv\) [a]
+
+[0]Applying instance of rewrite rule
+?x2 # ?t1 = ?t1 \(\equiv\) False
+
+[0]Rewriting:
+[a] = [] \(\equiv\) False
 \end{ttbox}
-
-The trace lists each rule being applied, both in its general form and the 
-instance being used.  For conditional rules, the trace lists the rule
-it is trying to rewrite and gives the result of attempting to prove
-each of the rule's conditions.  Many other hints about the simplifier's
-actions will appear.
+The trace lists each rule being applied, both in its general form and
+the instance being used. The \texttt{[}$i$\texttt{]} in front (where
+above $i$ is always \texttt{0}) indicates that we are inside the $i$th
+recursive invocation of the simplifier. Each attempt to apply a
+conditional rule shows the rule followed by the trace of the
+(recursive!) simplification of the conditions, the latter prefixed by
+\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
+Another source of recursive invocations of the simplifier are
+proofs of arithmetic formulae.
 
-In more complicated cases, the trace can be quite lengthy.  Invocations of the
-simplifier are often nested, for instance when solving conditions of rewrite
-rules.  Thus it is advisable to reset it:
-*}
+Many other hints about the simplifier's actions may appear.
 
-ML "reset trace_simp"
+In more complicated cases, the trace can be very lengthy.  Thus it is
+advisable to reset the \textsf{Trace Simplifier} flag after having
+obtained the desired trace.  *}
 
 (*<*)
 end
diff -r 2e2a506553a3 -r af7239e3054d doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Jun 10 17:59:12 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jun 10 18:36:47 2005 +0200
@@ -634,14 +634,18 @@
 as $\exists x.\,P$, they let us proceed with a proof.  They can be 
 filled in later, sometimes in stages and often automatically. 
 
-If unification fails when you think it should succeed, try setting the flag \index{flags}\isa{trace_unify_fail}\index{*trace_unify_fail (flag)},
-which makes Isabelle show the cause of unification failures.  For example, suppose we are trying to prove this subgoal by assumption:
+\begin{pgnote}
+If unification fails when you think it should succeed, try setting the Proof General flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
+\textsf{Trace Unification},
+which makes Isabelle show the cause of unification failures (in Proof
+General's \textsf{Trace} buffer).
+\end{pgnote}
+For example, suppose we are trying to prove this subgoal by assumption:
 \begin{isabelle}
 \ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a)
 \end{isabelle}
 The \isa{assumption} method having failed, we try again with the flag set:
 \begin{isabelle}
-\isacommand{ML}\ "set\ trace\_unify\_fail"\isanewline
 \isacommand{apply} assumption
 \end{isabelle}
 Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information:
diff -r 2e2a506553a3 -r af7239e3054d doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Fri Jun 10 17:59:12 2005 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jun 10 18:36:47 2005 +0200
@@ -309,6 +309,7 @@
 
 
 \subsection{The Types of Rational, Real and Complex Numbers}
+\label{sec:real}
 
 \index{rational numbers|(}\index{*rat (type)|(}%
 \index{real numbers|(}\index{*real (type)|(}%
@@ -340,15 +341,12 @@
 is performed.
 
 \begin{warn}
-Type \isa{real} is only available in the logic HOL-Complex, which
-is  HOL extended with a definitional development of the real and complex
-numbers.  Base your theory upon theory
-\thydx{Complex_Main}, not the usual \isa{Main}.%
+Type \isa{real} is only available in the logic HOL-Complex, which is
+HOL extended with a definitional development of the real and complex
+numbers.  Base your theory upon theory \thydx{Complex_Main}, not the
+usual \isa{Main}, and set the Proof General menu item \textsf{Isabelle} $>$
+\textsf{Logics} $>$ \textsf{HOL-Complex}.%
 \index{real numbers|)}\index{*real (type)|)}
-Launch Isabelle using the command 
-\begin{verbatim}
-Isabelle -l HOL-Complex
-\end{verbatim}
 \end{warn}
 
 Also available in HOL-Complex is the
diff -r 2e2a506553a3 -r af7239e3054d doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Fri Jun 10 17:59:12 2005 +0200
+++ b/doc-src/TutorialI/basics.tex	Fri Jun 10 18:36:47 2005 +0200
@@ -87,10 +87,10 @@
 \begin{center}\small
     \url{http://isabelle.in.tum.de/library/HOL/}
 \end{center}
-and is recommended browsing.
-There is also a growing Library~\cite{HOL-Library}\index{Library}
-of useful theories that are not part of \isa{Main} but can be included
-among the parents of a theory and will then be loaded automatically.
+and is recommended browsing. In subdirectory \texttt{Library} you find
+a growing library of useful theories that are not part of \isa{Main}
+but can be included among the parents of a theory and will then be
+loaded automatically.
 
 For the more adventurous, there is the \emph{Archive of Formal Proofs},
 a journal-like collection of more advanced Isabelle theories:
@@ -134,15 +134,17 @@
 \end{description}
 \begin{warn}
   Types are extremely important because they prevent us from writing
-  nonsense.  Isabelle insists that all terms and formulae must be well-typed
-  and will print an error message if a type mismatch is encountered. To
-  reduce the amount of explicit type information that needs to be provided by
-  the user, Isabelle infers the type of all variables automatically (this is
-  called \bfindex{type inference}) and keeps quiet about it. Occasionally
-  this may lead to misunderstandings between you and the system. If anything
-  strange happens, we recommend that you ask Isabelle to display all type
-  information. This is best done through the Proof General interface; see
-  \S\ref{sec:interface} for details.
+  nonsense.  Isabelle insists that all terms and formulae must be
+  well-typed and will print an error message if a type mismatch is
+  encountered. To reduce the amount of explicit type information that
+  needs to be provided by the user, Isabelle infers the type of all
+  variables automatically (this is called \bfindex{type inference})
+  and keeps quiet about it. Occasionally this may lead to
+  misunderstandings between you and the system. If anything strange
+  happens, we recommend that you ask Isabelle to display all type
+  information via the Proof General menu item \textsf{Isabelle} $>$
+  \textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface}
+  for details).
 \end{warn}%
 \index{types|)}
 
@@ -257,16 +259,13 @@
 the appendix.
 
 \begin{warn}
-A particular
-problem for novices can be the priority of operators. If you are unsure, use
-additional parentheses. In those cases where Isabelle echoes your
-input, you can see which parentheses are dropped --- they were superfluous. If
-you are unsure how to interpret Isabelle's output because you don't know
-where the (dropped) parentheses go, set the flag\index{flags}
-\isa{show_brackets}\index{*show_brackets (flag)}:
-\begin{ttbox}
-ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
-\end{ttbox}
+A particular problem for novices can be the priority of operators. If
+you are unsure, use additional parentheses. In those cases where
+Isabelle echoes your input, you can see which parentheses are dropped
+--- they were superfluous. If you are unsure how to interpret
+Isabelle's output because you don't know where the (dropped)
+parentheses go, set the Proof General flag \textsf{Isabelle} $>$
+\textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}).
 \end{warn}
 
 
@@ -304,48 +303,52 @@
 \section{Interaction and Interfaces}
 \label{sec:interface}
 
-Interaction with Isabelle can either occur at the shell level or through more
-advanced interfaces. To keep the tutorial independent of the interface, we
-have phrased the description of the interaction in a neutral language. For
-example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
-shell level, which is explained the first time the phrase is used. Other
-interfaces perform the same act by cursor movements and/or mouse clicks.
-Although shell-based interaction is quite feasible for the kind of proof
-scripts currently presented in this tutorial, the recommended interface for
-Isabelle/Isar is the Emacs-based \bfindex{Proof
-  General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
+The recommended interface for Isabelle/Isar is the (X)Emacs-based
+\bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}.
+Interaction with Isabelle at the shell level, although possible,
+should be avoided. Most of the tutorial is independent of the
+interface and is phrased in a neutral language. For example, the
+phrase ``to abandon a proof'' corresponds to the obvious
+action of clicking on the \textsf{Undo} symbol in Proof General.
+Proof General specific information is often displayed in paragraphs
+identified by a miniature Proof General icon. Here are two examples:
+\begin{pgnote}
+Proof General supports a special font with mathematical symbols known
+as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for
+example, you can enter either \verb!&!  or \verb!\<and>! to obtain
+$\land$. For a list of the most frequent symbols see table~\ref{tab:ascii}
+in the appendix.
 
-\begin{pgnote}
-Proof General specific information is always displayed in paragraphs
-identified by this miniature Proof General icon.
-
-On particularly nice feature of Proof General is its support for a special
-fonts with mathematical symbols. Most symbols have
-\textsc{ascii}-equivalents: for example, you can enter either \verb!&!
-or \verb!\<and>! to obtain $\land$. For a list of the most frequent symbols
-see table~\ref{tab:ascii} in the appendix.
+Note that by default x-symbols are not enabled. You have to switch
+them on via the menu item \textsf{Proof-General} $>$ \textsf{Options} $>$
+\textsf{X-Symbols} (and save the option via the top-level
+\textsf{Options} menu).
 \end{pgnote}
 
 \begin{pgnote}
-Proof General offers an \texttt{Isabelle} menu for displaying information
-and setting flags. A particularly useful flag is \texttt{Show Types}
-which causes Isabelle to output the type information that is usually
+Proof General offers the \textsf{Isabelle} menu for displaying
+information and setting flags. A particularly useful flag is
+\textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which
+causes Isabelle to output the type information that is usually
 suppressed. This is indispensible in case of errors of all kinds
-because often the types reveal the source of the problem. Once you have
-diagnosed the problem you may no longer want to see the types because they
-clutter all output. Simply reset the flag.
+because often the types reveal the source of the problem. Once you
+have diagnosed the problem you may no longer want to see the types
+because they clutter all output. Simply reset the flag.
 \end{pgnote}
 
 \section{Getting Started}
 
-Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
-  -I HOL} in a shell window.\footnote{Simply executing \texttt{isabelle -I}
-  starts the default logic, which usually is already \texttt{HOL}.  This is
-  controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
-    System Manual} for more details.} This presents you with Isabelle's most
-basic \textsc{ascii} interface.  In addition you need to open an editor window to
-create theory files.  While you are developing a theory, we recommend that you
-type each command into the file first and then enter it into Isabelle by
-copy-and-paste, thus ensuring that you have a complete record of your theory.
-As mentioned above, Proof General offers a much superior interface.
-If you have installed Proof General, you can start it by typing \texttt{Isabelle}.
+Assuming you have installed Isabelle and Proof General, you start it by typing
+\texttt{Isabelle} in a shell window. This launches a Proof General window.
+By default, you are in HOL\footnote{This is controlled by the
+\texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual}
+for more details.}.
+
+\begin{pgnote}
+You can choose a different logic via the \textsf{Isabelle} $>$
+\textsf{Logics} menu. For example, you may want to work in the real
+numbers, an extension of HOL (see \S\ref{sec:real}).
+% This is just excess baggage:
+%(You have to restart Proof General if you only compile the new logic
+%after having launching Proof General already).
+\end{pgnote}
diff -r 2e2a506553a3 -r af7239e3054d doc-src/TutorialI/tutorial.tex
--- a/doc-src/TutorialI/tutorial.tex	Fri Jun 10 17:59:12 2005 +0200
+++ b/doc-src/TutorialI/tutorial.tex	Fri Jun 10 18:36:47 2005 +0200
@@ -18,7 +18,6 @@
 \index{structural induction|see{induction, structural}}
 \index{termination|see{functions, total}}
 \index{tuples|see{pairs and tuples}}
-\index{settings|see{flags}}
 \index{*<*lex*>|see{lexicographic product}}
 
 \underscoreoff