# HG changeset patch
# User wenzelm
# Date 1415999625 -3600
# Node ID 059ba950a657e8c4a710991c43b04e0d0ca7b0a2
# Parent  16d92d37a8a1de2ed130aeac2e3b85f016758189# Parent  272d7fb92396f84348e3ce2bbbca4bbf44827d10
merged

diff -r 16d92d37a8a1 -r 059ba950a657 src/Doc/Functions/Functions.thy
--- a/src/Doc/Functions/Functions.thy	Fri Nov 14 18:39:42 2014 +0100
+++ b/src/Doc/Functions/Functions.thy	Fri Nov 14 22:13:45 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 16d92d37a8a1 -r 059ba950a657 src/Doc/Functions/document/root.tex
--- a/src/Doc/Functions/document/root.tex	Fri Nov 14 18:39:42 2014 +0100
+++ b/src/Doc/Functions/document/root.tex	Fri Nov 14 22:13:45 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 16d92d37a8a1 -r 059ba950a657 src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Fri Nov 14 18:39:42 2014 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Fri Nov 14 22:13:45 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
diff -r 16d92d37a8a1 -r 059ba950a657 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Nov 14 18:39:42 2014 +0100
+++ b/src/HOL/ROOT	Fri Nov 14 22:13:45 2014 +0100
@@ -19,7 +19,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false]
+  options [document = false, quick_and_dirty = false]
   theories Proofs (*sequential change of global flag!*)
   theories "~~/src/HOL/Library/Old_Datatype"
   files
@@ -400,7 +400,7 @@
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
-  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0]
+  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -425,7 +425,8 @@
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   *}
-  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0]
+  options [document_graph, print_mode = "no_brackets", parallel_proofs = 0,
+    quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Int"
   theories
diff -r 16d92d37a8a1 -r 059ba950a657 src/Pure/Concurrent/par_list_sequential.ML
--- a/src/Pure/Concurrent/par_list_sequential.ML	Fri Nov 14 18:39:42 2014 +0100
+++ b/src/Pure/Concurrent/par_list_sequential.ML	Fri Nov 14 22:13:45 2014 +0100
@@ -10,6 +10,7 @@
 fun managed_results _ f = map (Exn.capture f);
 fun map_name _ = map;
 val map = map;
+val map_independent = map;
 val get_some = get_first;
 val find_some = find_first;
 val exists = exists;