# HG changeset patch
# User nipkow
# Date 1118939154 -7200
# Node ID 50eab0183aea7151dbb9c6a17b8c90b73e24c759
# Parent  04cc6b4b3439ee03b7a1aea3fafbe42edbe3ce38
*** empty log message ***

diff -r 04cc6b4b3439 -r 50eab0183aea doc-src/TutorialI/Inductive/AB.thy
--- a/doc-src/TutorialI/Inductive/AB.thy	Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Inductive/AB.thy	Thu Jun 16 18:25:54 2005 +0200
@@ -101,7 +101,7 @@
 right increases or decreases the difference by 1, we must have passed through
 1 on our way from 0 to 2. Formally, we appeal to the following discrete
 intermediate value theorem @{thm[source]nat0_intermed_int_val}
-@{thm[display]nat0_intermed_int_val[no_vars]}
+@{thm[display,margin=60]nat0_intermed_int_val[no_vars]}
 where @{term f} is of type @{typ"nat \<Rightarrow> int"}, @{typ int} are the integers,
 @{text"\<bar>.\<bar>"} is the absolute value function\footnote{See
 Table~\ref{tab:ascii} in the Appendix for the correct \textsc{ascii}
diff -r 04cc6b4b3439 -r 50eab0183aea doc-src/TutorialI/Inductive/document/AB.tex
--- a/doc-src/TutorialI/Inductive/document/AB.tex	Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Thu Jun 16 18:25:54 2005 +0200
@@ -110,7 +110,8 @@
 1 on our way from 0 to 2. Formally, we appeal to the following discrete
 intermediate value theorem \isa{nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val}
 \begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isacharless}n{\isachardot}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k%
+\ \ \ \ \ {\isasymlbrakk}{\isasymforall}i{\isacharless}n{\isachardot}\ {\isasymbar}f\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharminus}\ f\ i{\isasymbar}\ {\isasymle}\ {\isadigit{1}}{\isacharsemicolon}\ f\ {\isadigit{0}}\ {\isasymle}\ k{\isacharsemicolon}\ k\ {\isasymle}\ f\ n{\isasymrbrakk}\isanewline
+\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isasymexists}i{\isasymle}n{\isachardot}\ f\ i\ {\isacharequal}\ k%
 \end{isabelle}
 where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
 \isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function\footnote{See
diff -r 04cc6b4b3439 -r 50eab0183aea doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Rules/rules.tex	Thu Jun 16 18:25:54 2005 +0200
@@ -640,6 +640,7 @@
 which makes Isabelle show the cause of unification failures (in Proof
 General's \textsf{Trace} buffer).
 \end{pgnote}
+\noindent
 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)
@@ -648,10 +649,9 @@
 \begin{isabelle}
 \isacommand{apply} assumption
 \end{isabelle}
-Even in this trivial case, the output is unexpectedly verbose, but it yields the necessary information that \isa{e} clashes with \isa{c}:
+In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}:
 \begin{isabelle}
-Clash: e =/= c\isanewline
-Clash: == =/= Trueprop
+Clash: e =/= c
 \end{isabelle}
 
 Isabelle uses
diff -r 04cc6b4b3439 -r 50eab0183aea doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex	Thu Jun 16 18:25:54 2005 +0200
@@ -398,10 +398,13 @@
 \rulename{mult_cancel_right}
 \end{isabelle}
 Theorems \isa{field_mult_eq_0_iff} and \isa{field_mult_cancel_right}
-express the same properties, only for fields. When working with such
-theorems, setting the \texttt{show_sorts}\index{*show_sorts (flag)}
-flag will display the type classes of all type variables. Here is how the 
-theorem \isa{field_mult_cancel_right} appears with the flag set.
+express the same properties, only for fields.
+\begin{pgnote}
+Setting the flag \textsf{Isabelle} $>$ \textsf{Settings} $>$
+\textsf{Show Sorts} will display the type classes of all type variables.
+\end{pgnote}
+\noindent
+Here is how the theorem \isa{field_mult_cancel_right} appears with the flag set.
 \begin{isabelle}
 ((a::'a::field)\ *\ (c::'a::field)\ =\ (b::'a::field)\ *\ c)\ =\isanewline
 (c\ =\ (0::'a::field)\ \isasymor \ a\ =\ b)
diff -r 04cc6b4b3439 -r 50eab0183aea doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Thu Jun 16 11:38:52 2005 +0200
+++ b/doc-src/TutorialI/fp.tex	Thu Jun 16 18:25:54 2005 +0200
@@ -90,73 +90,26 @@
 
 The most useful auxiliary commands are as follows:
 \begin{description}
-\item[Undoing:] \commdx{undo} undoes the effect of
-the
-  last command; \isacommand{undo} can be undone by
-  \commdx{redo}.  Both are only needed at the shell
-  level and should not occur in the final theory.
-\item[Printing the current state:] \commdx{pr}
-redisplays
-  the current proof state, for example when it has scrolled past the top of
-  the screen.
-\item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
-  print only the first $n$ subgoals from now on and redisplays the current
-  proof state. This is helpful when there are many subgoals.
 \item[Modifying the order of subgoals:]
 \commdx{defer} moves the first subgoal to the end and
 \commdx{prefer}~$n$ moves subgoal $n$ to the front.
 \item[Printing theorems:]
   \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
   prints the named theorems.
-\item[Displaying types:] We have already mentioned the flag
-  \texttt{show_types} above.\index{*show_types (flag)}
-  It can also be useful for detecting misspellings in
-  formulae. For example, if \texttt{show_types} is set and the goal
-  \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output
-\par\noindent
-\begin{isabelle}%
-variables:\isanewline
-~~xs~::~'a~list
-\end{isabelle}%
-\par\noindent
-which tells us that Isabelle has correctly inferred that
-\isa{xs} is a variable of list type. On the other hand, had we
-made a typo as in \isa{rev(re xs) = xs}, the response
-\par\noindent
-\begin{isabelle}%
-variables:\isanewline
-~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
-~~xs~::~'a~list%
-\end{isabelle}%
-\par\noindent
-would have alerted us because of the unexpected variable \isa{re}.
 \item[Reading terms and types:] \commdx{term}
   \textit{string} reads, type-checks and prints the given string as a term in
   the current context; the inferred type is output as well.
   \commdx{typ} \textit{string} reads and prints the given
   string as a type in the current context.
-\item[(Re)loading theories:] When you start your interaction you must open a
-  named theory with \commdx{theory}~\isa{T} \isacommand{imports} \dots
-  \isacommand{begin}. Isabelle automatically loads all the required parent
-  theories from their respective files (which may take a moment, unless the
-  theories are already loaded and the files have not been modified).
-  
-  If you suddenly discover that you need to modify a parent theory of your
-  current theory, you must first abandon your current theory%
-  \indexbold{abandoning a theory}\indexbold{theories!abandoning} (at the
-  shell level type \commdx{kill}). After the parent theory has been modified,
-  you go back to your original theory. When its opening
-  \isacommand{theory}~\isa{T} \dots \isacommand{begin} is processed, the
-  modified parent is reloaded automatically.
-  
-%  The only time when you need to load a theory by hand is when you simply
-%  want to check if it loads successfully without wanting to make use of the
-%  theory itself. This you can do by typing
-%  \isa{\commdx{use\_thy}~"T"}.
 \end{description}
 Further commands are found in the Isabelle/Isar Reference
 Manual~\cite{isabelle-isar-ref}.
 
+\begin{pgnote}
+Clicking on the \textsf{State} button redisplays the current proof state.
+This is helpful in case commands like \isacommand{thm} have overwritten it.
+\end{pgnote}
+
 We now examine Isabelle's functional programming constructs systematically,
 starting with inductive datatypes.