# HG changeset patch
# User wenzelm
# Date 1415981226 -3600
# Node ID 1c54ebc68394a9e1d525b44d7f999f50ec0b47b0
# Parent  6573e6d64ec89441ecf532affa8ef30790060c1e
use \isastyletext directly via 'text' command;

diff -r 6573e6d64ec8 -r 1c54ebc68394 src/Doc/Functions/Functions.thy
--- 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
diff -r 6573e6d64ec8 -r 1c54ebc68394 src/Doc/Functions/document/root.tex
--- 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}
 
diff -r 6573e6d64ec8 -r 1c54ebc68394 src/Doc/Tutorial/Documents/Documents.thy
--- 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