--- a/src/Doc/Functions/Functions.thy Fri Nov 14 11:19:14 2014 +0100
+++ b/src/Doc/Functions/Functions.thy Fri Nov 14 17:07:06 2014 +0100
@@ -100,7 +100,7 @@
lemma "map f (sep x ys) = sep (f x) (map f ys)"
apply (induct x ys rule: sep.induct)
-txt {*
+text {*
We get three cases, like in the definition.
@{subgoals [display]}
@@ -213,7 +213,7 @@
termination sum
apply (relation "measure (\<lambda>(i,N). N + 1 - i)")
-txt {*
+text {*
The \cmd{termination} command sets up the termination goal for the
specified function @{text "sum"}. If the function name is omitted, it
implicitly refers to the last function definition.
@@ -397,13 +397,13 @@
"even n = (n mod 2 = 0)"
"odd n = (n mod 2 = 1)"
-txt {*
+text {*
We apply simultaneous induction, specifying the induction variable
for both goals, separated by \cmd{and}: *}
apply (induct n and n rule: even_odd.induct)
-txt {*
+text {*
We get four subgoals, which correspond to the clauses in the
definition of @{const even} and @{const odd}:
@{subgoals[display,indent=0]}
@@ -413,7 +413,7 @@
apply simp_all
-txt {*
+text {*
@{subgoals[display,indent=0]}
\noindent These can be handled by Isabelle's arithmetic decision procedures.
@@ -437,7 +437,7 @@
"True"
apply (induct n rule: even_odd.induct)
-txt {*
+text {*
\noindent Now the third subgoal is a dead end, since we have no
useful induction hypothesis available:
@@ -585,7 +585,7 @@
| "And2 F p = F"
| "And2 X X = X"
-txt {*
+text {*
\noindent Now let's look at the proof obligations generated by a
function definition. In this case, they are:
@@ -603,7 +603,7 @@
apply pat_completeness
-txt {*
+text {*
The remaining subgoals express \emph{pattern compatibility}. We do
allow that an input value matches multiple patterns, but in this
case, the result (i.e.~the right hand sides of the equations) must
@@ -636,7 +636,7 @@
| "fib2 1 = 1"
| "fib2 (n + 2) = fib2 n + fib2 (Suc n)"
-txt {*
+text {*
This kind of matching is again justified by the proof of pattern
completeness and compatibility.
The proof obligation for pattern completeness states that every natural number is
@@ -807,12 +807,12 @@
lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0"
-txt {* \noindent We apply induction as usual, but using the partial induction
+text {* \noindent We apply induction as usual, but using the partial induction
rule: *}
apply (induct f n rule: findzero.pinduct)
-txt {* \noindent This gives the following subgoals:
+text {* \noindent This gives the following subgoals:
@{subgoals[display,indent=0]}
@@ -1041,7 +1041,7 @@
apply (relation "measure (\<lambda>n. n)")
apply auto
-txt {*
+text {*
We get stuck with the subgoal
@{subgoals[display]}
@@ -1140,7 +1140,7 @@
*}
termination proof
- txt {*
+ text {*
As usual, we have to give a wellfounded relation, such that the
arguments of the recursive calls get smaller. But what exactly are
--- a/src/Doc/Functions/document/root.tex Fri Nov 14 11:19:14 2014 +0100
+++ b/src/Doc/Functions/document/root.tex Fri Nov 14 17:07:06 2014 +0100
@@ -51,7 +51,6 @@
\author{Alexander Krauss}
\isabellestyle{tt}
-\renewcommand{\isastyletxt}{\isastyletext}% use same formatting for txt and text
\begin{document}
--- a/src/Doc/Tutorial/Documents/Documents.thy Fri Nov 14 11:19:14 2014 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy Fri Nov 14 17:07:06 2014 +0100
@@ -503,19 +503,12 @@
single argument).
\medskip Text blocks are introduced by the commands \bfindex{text}
- and \bfindex{txt}, for theory and proof contexts, respectively.
- Each takes again a single $text$ argument, which is interpreted as a
- free-form paragraph in {\LaTeX} (surrounded by some additional
- vertical space). This behavior may be changed by redefining the
- {\LaTeX} environments of \verb,isamarkuptext, or
- \verb,isamarkuptxt,, respectively (via \verb,\renewenvironment,) The
- text style of the body is determined by \verb,\isastyletext, and
- \verb,\isastyletxt,; the default setup uses a smaller font within
- proofs. This may be changed as follows:
-
-\begin{verbatim}
- \renewcommand{\isastyletxt}{\isastyletext}
-\end{verbatim}
+ and \bfindex{txt}. Each takes again a single $text$ argument,
+ which is interpreted as a free-form paragraph in {\LaTeX}
+ (surrounded by some additional vertical space). The typesetting
+ may be changed by redefining the {\LaTeX} environments of
+ \verb,isamarkuptext, or \verb,isamarkuptxt,, respectively
+ (via \verb,\renewenvironment,).
\medskip The $text$ part of Isabelle markup commands essentially
inserts \emph{quoted material} into a formal text, mainly for