--- 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.