merged
authorhaftmann
Mon Dec 21 21:34:14 2015 +0100 (2015-12-21 ago)
changeset 618925c68d06f97b3
parent 61859 76189756ff65
parent 61891 42d902e074e8
child 61894 f5a2aed23206
merged
NEWS
     1.1 --- a/Admin/components/bundled-windows	Sat Dec 19 17:03:17 2015 +0100
     1.2 +++ b/Admin/components/bundled-windows	Mon Dec 21 21:34:14 2015 +0100
     1.3 @@ -1,3 +1,3 @@
     1.4  #additional components to be bundled for release
     1.5 -cygwin-20151210
     1.6 +cygwin-20151221
     1.7  windows_app-20150821
     2.1 --- a/Admin/components/components.sha1	Sat Dec 19 17:03:17 2015 +0100
     2.2 +++ b/Admin/components/components.sha1	Mon Dec 21 21:34:14 2015 +0100
     2.3 @@ -18,6 +18,7 @@
     2.4  629b8fbe35952d1551cd2a7ff08db697f6dff870  cygwin-20141024.tar.gz
     2.5  ce93d0b3b2743c4f4e5bba30c2889b3b7bc22f2c  cygwin-20150410.tar.gz
     2.6  fa712dd5ec66ad16add1779d68aa171ff5694064  cygwin-20151210.tar.gz
     2.7 +056b843d5a3b69ecf8a52c06f2ce6e696dd275f9  cygwin-20151221.tar.gz
     2.8  0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
     2.9  2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
    2.10  e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
     3.1 --- a/Admin/lib/Tools/makedist_cygwin	Sat Dec 19 17:03:17 2015 +0100
     3.2 +++ b/Admin/lib/Tools/makedist_cygwin	Mon Dec 21 21:34:14 2015 +0100
     3.3 @@ -55,7 +55,7 @@
     3.4    --site "$CYGWIN_MIRROR" --no-verify \
     3.5    --local-package-dir 'C:\temp' \
     3.6    --root "$(cygpath -w "$TARGET")" \
     3.7 -  --packages perl,perl-libwww-perl,rlwrap,unzip,vim \
     3.8 +  --packages perl,perl-libwww-perl,rlwrap,unzip,nano \
     3.9    --no-shortcuts --no-startmenu --no-desktop --quiet-mode
    3.10  
    3.11  [ "$?" = 0 -a -e "$TARGET/etc" ] || exit 2
    3.12 @@ -68,8 +68,6 @@
    3.13    rm -f "$TARGET/etc/$NAME"
    3.14  done
    3.15  
    3.16 -ln -s cygperl5_14.dll "$TARGET/bin/cygperl5_14_2.dll"
    3.17 -
    3.18  rm "$TARGET/Cygwin.bat"
    3.19  
    3.20  
     4.1 --- a/NEWS	Sat Dec 19 17:03:17 2015 +0100
     4.2 +++ b/NEWS	Mon Dec 21 21:34:14 2015 +0100
     4.3 @@ -672,6 +672,13 @@
     4.4  tools, but can also cause INCOMPATIBILITY for tools that don't observe
     4.5  the proof context discipline.
     4.6  
     4.7 +* The following combinators for low-level profiling of the ML runtime
     4.8 +system are available:
     4.9 +
    4.10 +  profile_time          (*CPU time*)
    4.11 +  profile_time_thread   (*CPU time on this thread*)
    4.12 +  profile_allocations   (*overall heap allocations*)
    4.13 +
    4.14  
    4.15  *** System ***
    4.16  
     5.1 --- a/etc/options	Sat Dec 19 17:03:17 2015 +0100
     5.2 +++ b/etc/options	Mon Dec 21 21:34:14 2015 +0100
     5.3 @@ -125,7 +125,7 @@
     5.4  public option editor_output_delay : real = 0.1
     5.5    -- "delay for prover output (markup, common messages etc.)"
     5.6  
     5.7 -public option editor_prune_delay : real = 60.0
     5.8 +public option editor_prune_delay : real = 30.0
     5.9    -- "delay to prune history (delete old versions)"
    5.10  
    5.11  public option editor_update_delay : real = 0.5
     6.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Sat Dec 19 17:03:17 2015 +0100
     6.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Mon Dec 21 21:34:14 2015 +0100
     6.3 @@ -102,8 +102,8 @@
     6.4    apply} sequences.
     6.5  
     6.6    The current goal state, which is essentially a hidden part of the Isar/VM
     6.7 -  configurtation, is turned into a proof context and remaining conclusion.
     6.8 -  This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
     6.9 +  configuration, is turned into a proof context and remaining conclusion.
    6.10 +  This corresponds to @{command fix}~/ @{command assume}~/ @{command show} in
    6.11    structured proofs, but the text of the parameters, premises and conclusion
    6.12    is not given explicitly.
    6.13  
     7.1 --- a/src/Doc/antiquote_setup.ML	Sat Dec 19 17:03:17 2015 +0100
     7.2 +++ b/src/Doc/antiquote_setup.ML	Mon Dec 21 21:34:14 2015 +0100
     7.3 @@ -130,13 +130,15 @@
     7.4                Output.output
     7.5                  (Thy_Output.string_of_margin ctxt
     7.6                    (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
     7.7 -              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
     7.8 +              "\\rulename{" ^
     7.9 +              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    7.10              #> space_implode "\\par\\smallskip%\n"
    7.11              #> Latex.environment "isabelle"
    7.12            else
    7.13              map (fn (p, name) =>
    7.14 -              Output.output (Pretty.str_of p) ^
    7.15 -              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    7.16 +              Output.output (Pretty.unformatted_string_of p) ^
    7.17 +              "\\rulename{" ^
    7.18 +              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
    7.19              #> space_implode "\\par\\smallskip%\n"
    7.20              #> enclose "\\isa{" "}")));
    7.21  
     8.1 --- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sat Dec 19 17:03:17 2015 +0100
     8.2 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Dec 21 21:34:14 2015 +0100
     8.3 @@ -11,8 +11,8 @@
     8.4  subsection \<open>Continuous linear forms\<close>
     8.5  
     8.6  text \<open>
     8.7 -  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>,
     8.8 -  iff it is bounded, i.e.
     8.9 +  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>, iff
    8.10 +  it is bounded, i.e.
    8.11    \begin{center}
    8.12    \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
    8.13    \end{center}
    8.14 @@ -52,20 +52,20 @@
    8.15    \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
    8.16    \end{center}
    8.17  
    8.18 -  For the case \<open>V = {0}\<close> the supremum would be taken from an empty set.
    8.19 -  Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this
    8.20 -  situation it must be guaranteed that there is an element in this set. This
    8.21 -  element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties.
    8.22 -  Furthermore it does not have to change the norm in all other cases, so it
    8.23 -  must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>.
    8.24 +  For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since
    8.25 +  \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it
    8.26 +  must be guaranteed that there is an element in this set. This element must
    8.27 +  be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does
    8.28 +  not have to change the norm in all other cases, so it must be \<open>0\<close>, as all
    8.29 +  other elements are \<open>{} \<ge> 0\<close>.
    8.30  
    8.31    Thus we define the set \<open>B\<close> where the supremum is taken from as follows:
    8.32    \begin{center}
    8.33    \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
    8.34    \end{center}
    8.35  
    8.36 -  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists
    8.37 -  (otherwise it is undefined).
    8.38 +  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise
    8.39 +  it is undefined).
    8.40  \<close>
    8.41  
    8.42  locale fn_norm =
     9.1 --- a/src/HOL/Hahn_Banach/Function_Order.thy	Sat Dec 19 17:03:17 2015 +0100
     9.2 +++ b/src/HOL/Hahn_Banach/Function_Order.thy	Mon Dec 21 21:34:14 2015 +0100
     9.3 @@ -11,14 +11,12 @@
     9.4  subsection \<open>The graph of a function\<close>
     9.5  
     9.6  text \<open>
     9.7 -  We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with
     9.8 -  domain \<open>F\<close> as the set
     9.9 +  We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with domain \<open>F\<close> as the set
    9.10    \begin{center}
    9.11    \<open>{(x, f x). x \<in> F}\<close>
    9.12    \end{center}
    9.13 -  So we are modeling partial functions by specifying the domain and
    9.14 -  the mapping function. We use the term ``function'' also for its
    9.15 -  graph.
    9.16 +  So we are modeling partial functions by specifying the domain and the
    9.17 +  mapping function. We use the term ``function'' also for its graph.
    9.18  \<close>
    9.19  
    9.20  type_synonym 'a graph = "('a \<times> real) set"
    9.21 @@ -41,8 +39,8 @@
    9.22  subsection \<open>Functions ordered by domain extension\<close>
    9.23  
    9.24  text \<open>
    9.25 -  A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of
    9.26 -  \<open>h\<close> is a subset of the graph of \<open>h'\<close>.
    9.27 +  A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of \<open>h\<close> is a subset of
    9.28 +  the graph of \<open>h'\<close>.
    9.29  \<close>
    9.30  
    9.31  lemma graph_extI:
    9.32 @@ -93,8 +91,8 @@
    9.33  subsection \<open>Norm-preserving extensions of a function\<close>
    9.34  
    9.35  text \<open>
    9.36 -  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The
    9.37 -  set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
    9.38 +  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The set
    9.39 +  of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
    9.40    bounded by \<open>p\<close>, is defined as follows.
    9.41  \<close>
    9.42  
    10.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sat Dec 19 17:03:17 2015 +0100
    10.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Dec 21 21:34:14 2015 +0100
    10.3 @@ -18,28 +18,26 @@
    10.4  
    10.5  paragraph \<open>Hahn-Banach Theorem.\<close>
    10.6  text \<open>
    10.7 -  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
    10.8 -  on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded
    10.9 -  by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear
   10.10 -  form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded
   10.11 -  by \<open>p\<close>.
   10.12 +  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on
   10.13 +  \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded by
   10.14 +  \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close>
   10.15 +  on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded by \<open>p\<close>.
   10.16  \<close>
   10.17  
   10.18  paragraph \<open>Proof Sketch.\<close>
   10.19  text \<open>
   10.20 -  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
   10.21 -  of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
   10.22 +  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces of
   10.23 +  \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
   10.24  
   10.25    \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
   10.26  
   10.27 -  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in
   10.28 -  \<open>M\<close>.
   10.29 +  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in \<open>M\<close>.
   10.30  
   10.31    \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
   10.32    contradiction:
   10.33  
   10.34 -    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in
   10.35 -    a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
   10.36 +    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in a
   10.37 +    norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
   10.38  
   10.39      \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
   10.40  \<close>
   10.41 @@ -292,14 +290,13 @@
   10.42  
   10.43  text \<open>
   10.44    The following alternative formulation of the Hahn-Banach
   10.45 -  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form
   10.46 -  \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are
   10.47 -  equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff}
   10.48 -  (see page \pageref{abs-ineq-iff}).}
   10.49 +  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form \<open>f\<close>
   10.50 +  and a seminorm \<open>p\<close> the following inequality are equivalent:\footnote{This
   10.51 +  was shown in lemma @{thm [source] abs_ineq_iff} (see page
   10.52 +  \pageref{abs-ineq-iff}).}
   10.53    \begin{center}
   10.54    \begin{tabular}{lll}
   10.55 -  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
   10.56 -  \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
   10.57 +  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
   10.58    \end{tabular}
   10.59    \end{center}
   10.60  \<close>
   10.61 @@ -336,9 +333,8 @@
   10.62  subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
   10.63  
   10.64  text \<open>
   10.65 -  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>,
   10.66 -  can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> =
   10.67 -  \<parallel>g\<parallel>\<close>.
   10.68 +  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, can
   10.69 +  be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>.
   10.70  \<close>
   10.71  
   10.72  theorem norm_Hahn_Banach:
   10.73 @@ -420,10 +416,10 @@
   10.74           OF F_norm, folded B_def fn_norm_def])
   10.75    qed
   10.76  
   10.77 -  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we
   10.78 -    can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
   10.79 -    extended in a norm-preserving way to some function \<open>g\<close> on the whole
   10.80 -    vector space \<open>E\<close>.\<close>
   10.81 +  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we can
   10.82 +    apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
   10.83 +    extended in a norm-preserving way to some function \<open>g\<close> on the whole vector
   10.84 +    space \<open>E\<close>.\<close>
   10.85  
   10.86    with E FE linearform q obtain g where
   10.87        linearformE: "linearform E g"
    11.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sat Dec 19 17:03:17 2015 +0100
    11.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Dec 21 21:34:14 2015 +0100
    11.3 @@ -9,14 +9,13 @@
    11.4  begin
    11.5  
    11.6  text \<open>
    11.7 -  In this section the following context is presumed. Let \<open>E\<close> be a real
    11.8 -  vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close>
    11.9 -  a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
   11.10 -  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close>
   11.11 -  and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H'
   11.12 -  = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close>
   11.13 -  with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close>
   11.14 -  for a certain \<open>\<xi>\<close>.
   11.15 +  In this section the following context is presumed. Let \<open>E\<close> be a real vector
   11.16 +  space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear
   11.17 +  function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a superspace of
   11.18 +  \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is an
   11.19 +  element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' = H + lin x\<^sub>0\<close>, so
   11.20 +  for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is
   11.21 +  unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>.
   11.22  
   11.23    Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.
   11.24  
   11.25 @@ -82,8 +81,8 @@
   11.26  
   11.27  text \<open>
   11.28    \<^medskip>
   11.29 -  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where
   11.30 -  \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>.
   11.31 +  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close>
   11.32 +  is a linear extension of \<open>h\<close> to \<open>H'\<close>.
   11.33  \<close>
   11.34  
   11.35  lemma h'_lf:
    12.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Dec 19 17:03:17 2015 +0100
    12.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Dec 21 21:34:14 2015 +0100
    12.3 @@ -10,17 +10,16 @@
    12.4  
    12.5  text \<open>
    12.6    This section contains some lemmas that will be used in the proof of the
    12.7 -  Hahn-Banach Theorem. In this section the following context is presumed.
    12.8 -  Let \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a
    12.9 -  subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of
   12.10 -  norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will
   12.11 -  show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of
   12.12 -  the chain \<open>c\<close>.
   12.13 +  Hahn-Banach Theorem. In this section the following context is presumed. Let
   12.14 +  \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of
   12.15 +  \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of norm-preserving
   12.16 +  extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will show some properties
   12.17 +  about the limit function \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>.
   12.18  
   12.19    \<^medskip>
   12.20 -  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
   12.21 -  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of
   12.22 -  one of the elements of the chain.
   12.23 +  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let
   12.24 +  \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of one of
   12.25 +  the elements of the chain.
   12.26  \<close>
   12.27  
   12.28  lemmas [dest?] = chainsD
   12.29 @@ -55,10 +54,10 @@
   12.30  
   12.31  text \<open>
   12.32    \<^medskip>
   12.33 -  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
   12.34 -  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of
   12.35 -  the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>,
   12.36 -  such that \<open>h\<close> extends \<open>h'\<close>.
   12.37 +  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let
   12.38 +  \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of the
   12.39 +  supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such
   12.40 +  that \<open>h\<close> extends \<open>h'\<close>.
   12.41  \<close>
   12.42  
   12.43  lemma some_H'h':
   12.44 @@ -83,9 +82,9 @@
   12.45  
   12.46  text \<open>
   12.47    \<^medskip>
   12.48 -  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function
   12.49 -  \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close>
   12.50 -  extends \<open>h'\<close>.
   12.51 +  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function \<open>h\<close>
   12.52 +  are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends
   12.53 +  \<open>h'\<close>.
   12.54  \<close>
   12.55  
   12.56  lemma some_H'h'2:
   12.57 @@ -99,8 +98,8 @@
   12.58      \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
   12.59      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
   12.60  proof -
   12.61 -  txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>,
   12.62 -  such that \<open>h\<close> extends \<open>h''\<close>.\<close>
   12.63 +  txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close>
   12.64 +    extends \<open>h''\<close>.\<close>
   12.65  
   12.66    from M cM u and y obtain H' h' where
   12.67        y_hy: "(y, h y) \<in> graph H' h'"
   12.68 @@ -121,10 +120,9 @@
   12.69        "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
   12.70      by (rule some_H'h't [elim_format]) blast
   12.71  
   12.72 -  txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain,
   12.73 -    \<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both
   12.74 -    \<open>x\<close> and \<open>y\<close> are contained in the greater
   12.75 -    one. \label{cases1}\<close>
   12.76 +  txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an
   12.77 +    extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in
   12.78 +    the greater one. \label{cases1}\<close>
   12.79  
   12.80    from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
   12.81      by (blast dest: chainsD)
   12.82 @@ -205,11 +203,11 @@
   12.83  
   12.84  text \<open>
   12.85    \<^medskip>
   12.86 -  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close>
   12.87 -  is in the domain of a function \<open>h'\<close> in the chain of norm preserving
   12.88 -  extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function
   12.89 -  values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close>
   12.90 -  is linear by construction of \<open>M\<close>.
   12.91 +  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> is
   12.92 +  in the domain of a function \<open>h'\<close> in the chain of norm preserving extensions.
   12.93 +  Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function values of \<open>x\<close> are
   12.94 +  identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> is linear by
   12.95 +  construction of \<open>M\<close>.
   12.96  \<close>
   12.97  
   12.98  lemma sup_lf:
   12.99 @@ -286,8 +284,8 @@
  12.100  
  12.101  text \<open>
  12.102    \<^medskip>
  12.103 -  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is
  12.104 -  a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
  12.105 +  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is a
  12.106 +  subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
  12.107    properties follow from the fact that \<open>F\<close> is a vector space.
  12.108  \<close>
  12.109  
  12.110 @@ -367,8 +365,8 @@
  12.111  
  12.112  text \<open>
  12.113    \<^medskip>
  12.114 -  The limit function is bounded by the norm \<open>p\<close> as well, since all elements
  12.115 -  in the chain are bounded by \<open>p\<close>.
  12.116 +  The limit function is bounded by the norm \<open>p\<close> as well, since all elements in
  12.117 +  the chain are bounded by \<open>p\<close>.
  12.118  \<close>
  12.119  
  12.120  lemma sup_norm_pres:
  12.121 @@ -389,10 +387,10 @@
  12.122  
  12.123  text \<open>
  12.124    \<^medskip>
  12.125 -  The following lemma is a property of linear forms on real vector spaces.
  12.126 -  It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
  12.127 -  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces
  12.128 -  the following inequality are equivalent:
  12.129 +  The following lemma is a property of linear forms on real vector spaces. It
  12.130 +  will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
  12.131 +  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the
  12.132 +  following inequality are equivalent:
  12.133    \begin{center}
  12.134    \begin{tabular}{lll}
  12.135    \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
    13.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sat Dec 19 17:03:17 2015 +0100
    13.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Dec 21 21:34:14 2015 +0100
    13.3 @@ -11,9 +11,9 @@
    13.4  subsection \<open>Quasinorms\<close>
    13.5  
    13.6  text \<open>
    13.7 -  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals
    13.8 -  that has the following properties: it is positive definite, absolute
    13.9 -  homogeneous and subadditive.
   13.10 +  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals that
   13.11 +  has the following properties: it is positive definite, absolute homogeneous
   13.12 +  and subadditive.
   13.13  \<close>
   13.14  
   13.15  locale seminorm =
   13.16 @@ -57,8 +57,7 @@
   13.17  subsection \<open>Norms\<close>
   13.18  
   13.19  text \<open>
   13.20 -  A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the
   13.21 -  \<open>0\<close> vector to \<open>0\<close>.
   13.22 +  A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the \<open>0\<close> vector to \<open>0\<close>.
   13.23  \<close>
   13.24  
   13.25  locale norm = seminorm +
   13.26 @@ -68,8 +67,7 @@
   13.27  subsection \<open>Normed vector spaces\<close>
   13.28  
   13.29  text \<open>
   13.30 -  A vector space together with a norm is called a \<^emph>\<open>normed
   13.31 -  space\<close>.
   13.32 +  A vector space together with a norm is called a \<^emph>\<open>normed space\<close>.
   13.33  \<close>
   13.34  
   13.35  locale normed_vectorspace = vectorspace + norm
    14.1 --- a/src/HOL/Hahn_Banach/Subspace.thy	Sat Dec 19 17:03:17 2015 +0100
    14.2 +++ b/src/HOL/Hahn_Banach/Subspace.thy	Mon Dec 21 21:34:14 2015 +0100
    14.3 @@ -139,8 +139,8 @@
    14.4  subsection \<open>Linear closure\<close>
    14.5  
    14.6  text \<open>
    14.7 -  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples
    14.8 -  of \<open>x\<close>.
    14.9 +  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples of
   14.10 +  \<open>x\<close>.
   14.11  \<close>
   14.12  
   14.13  definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
   14.14 @@ -318,7 +318,7 @@
   14.15    qed
   14.16  qed
   14.17  
   14.18 -text\<open>The sum of two subspaces is a vectorspace.\<close>
   14.19 +text \<open>The sum of two subspaces is a vectorspace.\<close>
   14.20  
   14.21  lemma sum_vs [intro?]:
   14.22      "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
   14.23 @@ -328,10 +328,10 @@
   14.24  subsection \<open>Direct sums\<close>
   14.25  
   14.26  text \<open>
   14.27 -  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the
   14.28 -  only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct
   14.29 -  sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and
   14.30 -  \<open>v \<in> V\<close> is unique.
   14.31 +  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the only
   14.32 +  common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct sum of
   14.33 +  \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is
   14.34 +  unique.
   14.35  \<close>
   14.36  
   14.37  lemma decomp:
   14.38 @@ -434,8 +434,8 @@
   14.39  
   14.40  text \<open>
   14.41    Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close>
   14.42 -  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique,
   14.43 -  it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
   14.44 +  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it
   14.45 +  follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
   14.46  \<close>
   14.47  
   14.48  lemma decomp_H'_H:
    15.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sat Dec 19 17:03:17 2015 +0100
    15.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Dec 21 21:34:14 2015 +0100
    15.3 @@ -23,13 +23,13 @@
    15.4  subsection \<open>Vector space laws\<close>
    15.5  
    15.6  text \<open>
    15.7 -  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with
    15.8 -  the following vector space laws: The set \<open>V\<close> is closed under addition and
    15.9 -  scalar multiplication, addition is associative and commutative; \<open>- x\<close> is
   15.10 -  the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of
   15.11 -  addition. Addition and multiplication are distributive; scalar
   15.12 -  multiplication is associative and the real number \<open>1\<close> is the neutral
   15.13 -  element of scalar multiplication.
   15.14 +  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with the
   15.15 +  following vector space laws: The set \<open>V\<close> is closed under addition and scalar
   15.16 +  multiplication, addition is associative and commutative; \<open>- x\<close> is the
   15.17 +  inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of addition.
   15.18 +  Addition and multiplication are distributive; scalar multiplication is
   15.19 +  associative and the real number \<open>1\<close> is the neutral element of scalar
   15.20 +  multiplication.
   15.21  \<close>
   15.22  
   15.23  locale vectorspace =
   15.24 @@ -78,8 +78,10 @@
   15.25  lemmas add_ac = add_assoc add_commute add_left_commute
   15.26  
   15.27  
   15.28 -text \<open>The existence of the zero element of a vector space follows from the
   15.29 -  non-emptiness of carrier set.\<close>
   15.30 +text \<open>
   15.31 +  The existence of the zero element of a vector space follows from the
   15.32 +  non-emptiness of carrier set.
   15.33 +\<close>
   15.34  
   15.35  lemma zero [iff]: "0 \<in> V"
   15.36  proof -
    16.1 --- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sat Dec 19 17:03:17 2015 +0100
    16.2 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Mon Dec 21 21:34:14 2015 +0100
    16.3 @@ -9,13 +9,13 @@
    16.4  begin
    16.5  
    16.6  text \<open>
    16.7 -  Zorn's Lemmas states: if every linear ordered subset of an ordered
    16.8 -  set \<open>S\<close> has an upper bound in \<open>S\<close>, then there exists a
    16.9 -  maximal element in \<open>S\<close>.  In our application, \<open>S\<close> is a
   16.10 -  set of sets ordered by set inclusion. Since the union of a chain of
   16.11 -  sets is an upper bound for all elements of the chain, the conditions
   16.12 -  of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it
   16.13 -  suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> also lies in \<open>S\<close>.
   16.14 +  Zorn's Lemmas states: if every linear ordered subset of an ordered set \<open>S\<close>
   16.15 +  has an upper bound in \<open>S\<close>, then there exists a maximal element in \<open>S\<close>. In
   16.16 +  our application, \<open>S\<close> is a set of sets ordered by set inclusion. Since the
   16.17 +  union of a chain of sets is an upper bound for all elements of the chain,
   16.18 +  the conditions of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it
   16.19 +  suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close>
   16.20 +  also lies in \<open>S\<close>.
   16.21  \<close>
   16.22  
   16.23  theorem Zorn's_Lemma:
   16.24 @@ -28,16 +28,14 @@
   16.25      fix c assume "c \<in> chains S"
   16.26      show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
   16.27      proof cases
   16.28 -
   16.29 -      txt \<open>If \<open>c\<close> is an empty chain, then every element in
   16.30 -        \<open>S\<close> is an upper bound of \<open>c\<close>.\<close>
   16.31 +      txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper
   16.32 +        bound of \<open>c\<close>.\<close>
   16.33  
   16.34        assume "c = {}"
   16.35        with aS show ?thesis by fast
   16.36  
   16.37 -      txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper
   16.38 -        bound of \<open>c\<close>, lying in \<open>S\<close>.\<close>
   16.39 -
   16.40 +      txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in
   16.41 +        \<open>S\<close>.\<close>
   16.42      next
   16.43        assume "c \<noteq> {}"
   16.44        show ?thesis
    17.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Dec 19 17:03:17 2015 +0100
    17.2 +++ b/src/HOL/Hilbert_Choice.thy	Mon Dec 21 21:34:14 2015 +0100
    17.3 @@ -6,7 +6,7 @@
    17.4  section \<open>Hilbert's Epsilon-Operator and the Axiom of Choice\<close>
    17.5  
    17.6  theory Hilbert_Choice
    17.7 -imports Nat Wellfounded
    17.8 +imports Wellfounded
    17.9  keywords "specification" :: thy_goal
   17.10  begin
   17.11  
    18.1 --- a/src/HOL/Library/ContNotDenum.thy	Sat Dec 19 17:03:17 2015 +0100
    18.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Dec 21 21:34:14 2015 +0100
    18.3 @@ -143,4 +143,20 @@
    18.4    using uncountable_open_interval [of a b]
    18.5    by (metis countable_Un_iff ivl_disj_un_singleton(4))
    18.6  
    18.7 +lemma real_interval_avoid_countable_set:
    18.8 +  fixes a b :: real and A :: "real set"
    18.9 +  assumes "a < b" and "countable A"
   18.10 +  shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
   18.11 +proof -
   18.12 +  from `countable A` have "countable (A \<inter> {a<..<b})" by auto
   18.13 +  moreover with `a < b` have "\<not> countable {a<..<b}" 
   18.14 +    by (simp add: uncountable_open_interval)
   18.15 +  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto
   18.16 +  hence "A \<inter> {a<..<b} \<subset> {a<..<b}" 
   18.17 +    by (intro psubsetI, auto)
   18.18 +  hence "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
   18.19 +    by (rule psubset_imp_ex_mem)
   18.20 +  thus ?thesis by auto
   18.21 +qed
   18.22 +
   18.23  end
    19.1 --- a/src/HOL/Library/Extended_Real.thy	Sat Dec 19 17:03:17 2015 +0100
    19.2 +++ b/src/HOL/Library/Extended_Real.thy	Mon Dec 21 21:34:14 2015 +0100
    19.3 @@ -2450,6 +2450,16 @@
    19.4  lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
    19.5    by (auto dest!: lim_real_of_ereal)
    19.6  
    19.7 +lemma convergent_real_imp_convergent_ereal:
    19.8 +  assumes "convergent a"
    19.9 +  shows "convergent (\<lambda>n. ereal (a n))" and "lim (\<lambda>n. ereal (a n)) = ereal (lim a)"
   19.10 +proof -
   19.11 +  from assms obtain L where L: "a ----> L" unfolding convergent_def ..
   19.12 +  hence lim: "(\<lambda>n. ereal (a n)) ----> ereal L" using lim_ereal by auto
   19.13 +  thus "convergent (\<lambda>n. ereal (a n))" unfolding convergent_def ..
   19.14 +  thus "lim (\<lambda>n. ereal (a n)) = ereal (lim a)" using lim L limI by metis
   19.15 +qed
   19.16 +
   19.17  lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
   19.18  proof -
   19.19    {
   19.20 @@ -3223,7 +3233,6 @@
   19.21    thus "(\<Sum>x. ereal (f x)) \<noteq> -\<infinity>" by simp_all
   19.22  qed
   19.23  
   19.24 -
   19.25  lemma SUP_ereal_add_directed:
   19.26    fixes f g :: "'a \<Rightarrow> ereal"
   19.27    assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
   19.28 @@ -3293,50 +3302,6 @@
   19.29      done
   19.30  qed
   19.31  
   19.32 -subsection \<open>More Limits\<close>
   19.33 -
   19.34 -lemma convergent_limsup_cl:
   19.35 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   19.36 -  shows "convergent X \<Longrightarrow> limsup X = lim X"
   19.37 -  by (auto simp: convergent_def limI lim_imp_Limsup)
   19.38 -
   19.39 -lemma lim_increasing_cl:
   19.40 -  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   19.41 -  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
   19.42 -proof
   19.43 -  show "f ----> (SUP n. f n)"
   19.44 -    using assms
   19.45 -    by (intro increasing_tendsto)
   19.46 -       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   19.47 -qed
   19.48 -
   19.49 -lemma lim_decreasing_cl:
   19.50 -  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   19.51 -  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
   19.52 -proof
   19.53 -  show "f ----> (INF n. f n)"
   19.54 -    using assms
   19.55 -    by (intro decreasing_tendsto)
   19.56 -       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   19.57 -qed
   19.58 -
   19.59 -lemma compact_complete_linorder:
   19.60 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   19.61 -  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
   19.62 -proof -
   19.63 -  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
   19.64 -    using seq_monosub[of X]
   19.65 -    unfolding comp_def
   19.66 -    by auto
   19.67 -  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
   19.68 -    by (auto simp add: monoseq_def)
   19.69 -  then obtain l where "(X \<circ> r) ----> l"
   19.70 -     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
   19.71 -     by auto
   19.72 -  then show ?thesis
   19.73 -    using \<open>subseq r\<close> by auto
   19.74 -qed
   19.75 -
   19.76  lemma ereal_dense3:
   19.77    fixes x y :: ereal
   19.78    shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
    20.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Sat Dec 19 17:03:17 2015 +0100
    20.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Mon Dec 21 21:34:14 2015 +0100
    20.3 @@ -351,5 +351,53 @@
    20.4    finally show ?thesis
    20.5      by (auto simp: Liminf_def)
    20.6  qed
    20.7 +subsection \<open>More Limits\<close>
    20.8 +
    20.9 +lemma convergent_limsup_cl:
   20.10 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   20.11 +  shows "convergent X \<Longrightarrow> limsup X = lim X"
   20.12 +  by (auto simp: convergent_def limI lim_imp_Limsup)
   20.13 +
   20.14 +lemma convergent_liminf_cl:
   20.15 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   20.16 +  shows "convergent X \<Longrightarrow> liminf X = lim X"
   20.17 +  by (auto simp: convergent_def limI lim_imp_Liminf)
   20.18 +
   20.19 +lemma lim_increasing_cl:
   20.20 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   20.21 +  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
   20.22 +proof
   20.23 +  show "f ----> (SUP n. f n)"
   20.24 +    using assms
   20.25 +    by (intro increasing_tendsto)
   20.26 +       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   20.27 +qed
   20.28 +
   20.29 +lemma lim_decreasing_cl:
   20.30 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   20.31 +  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
   20.32 +proof
   20.33 +  show "f ----> (INF n. f n)"
   20.34 +    using assms
   20.35 +    by (intro decreasing_tendsto)
   20.36 +       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   20.37 +qed
   20.38 +
   20.39 +lemma compact_complete_linorder:
   20.40 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   20.41 +  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
   20.42 +proof -
   20.43 +  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
   20.44 +    using seq_monosub[of X]
   20.45 +    unfolding comp_def
   20.46 +    by auto
   20.47 +  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
   20.48 +    by (auto simp add: monoseq_def)
   20.49 +  then obtain l where "(X \<circ> r) ----> l"
   20.50 +     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
   20.51 +     by auto
   20.52 +  then show ?thesis
   20.53 +    using \<open>subseq r\<close> by auto
   20.54 +qed
   20.55  
   20.56  end
    21.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Dec 19 17:03:17 2015 +0100
    21.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Dec 21 21:34:14 2015 +0100
    21.3 @@ -3391,6 +3391,60 @@
    21.4    ultimately show ?thesis by auto
    21.5  qed
    21.6  
    21.7 +lemma continuous_ge_on_Ioo:
    21.8 +  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
    21.9 +  shows "g (x::real) \<ge> (a::real)"
   21.10 +proof-
   21.11 +  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_greaterThanLessThan[symmetric])
   21.12 +  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
   21.13 +  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
   21.14 +  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
   21.15 +    by (auto simp: continuous_on_closed_vimage)
   21.16 +  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
   21.17 +  finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto 
   21.18 +qed 
   21.19 +
   21.20 +lemma interior_real_semiline':
   21.21 +  fixes a :: real
   21.22 +  shows "interior {..a} = {..<a}"
   21.23 +proof -
   21.24 +  {
   21.25 +    fix y
   21.26 +    assume "a > y"
   21.27 +    then have "y \<in> interior {..a}"
   21.28 +      apply (simp add: mem_interior)
   21.29 +      apply (rule_tac x="(a-y)" in exI)
   21.30 +      apply (auto simp add: dist_norm)
   21.31 +      done
   21.32 +  }
   21.33 +  moreover
   21.34 +  {
   21.35 +    fix y
   21.36 +    assume "y \<in> interior {..a}"
   21.37 +    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
   21.38 +      using mem_interior_cball[of y "{..a}"] by auto
   21.39 +    moreover from e have "y + e \<in> cball y e"
   21.40 +      by (auto simp add: cball_def dist_norm)
   21.41 +    ultimately have "a \<ge> y + e" by auto
   21.42 +    then have "a > y" using e by auto
   21.43 +  }
   21.44 +  ultimately show ?thesis by auto
   21.45 +qed
   21.46 +
   21.47 +lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
   21.48 +proof-
   21.49 +  have "{a..b} = {a..} \<inter> {..b}" by auto
   21.50 +  also have "interior ... = {a<..} \<inter> {..<b}" 
   21.51 +    by (simp add: interior_real_semiline interior_real_semiline')
   21.52 +  also have "... = {a<..<b}" by auto
   21.53 +  finally show ?thesis .
   21.54 +qed
   21.55 +
   21.56 +lemma frontier_real_Iic:
   21.57 +  fixes a :: real
   21.58 +  shows "frontier {..a} = {a}"
   21.59 +  unfolding frontier_def by (auto simp add: interior_real_semiline')
   21.60 +
   21.61  lemma rel_interior_real_box:
   21.62    fixes a b :: real
   21.63    assumes "a < b"
    22.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Sat Dec 19 17:03:17 2015 +0100
    22.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Dec 21 21:34:14 2015 +0100
    22.3 @@ -2451,6 +2451,20 @@
    22.4    unfolding has_vector_derivative_def
    22.5    by (rule has_derivative_at_within)
    22.6  
    22.7 +lemma has_vector_derivative_weaken:
    22.8 +  fixes x D and f g s t
    22.9 +  assumes f: "(f has_vector_derivative D) (at x within t)"
   22.10 +    and "x \<in> s" "s \<subseteq> t" 
   22.11 +    and "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
   22.12 +  shows "(g has_vector_derivative D) (at x within s)"
   22.13 +proof -
   22.14 +  have "(f has_vector_derivative D) (at x within s) \<longleftrightarrow> (g has_vector_derivative D) (at x within s)"
   22.15 +    unfolding has_vector_derivative_def has_derivative_iff_norm
   22.16 +    using assms by (intro conj_cong Lim_cong_within refl) auto
   22.17 +  then show ?thesis
   22.18 +    using has_vector_derivative_within_subset[OF f `s \<subseteq> t`] by simp
   22.19 +qed
   22.20 +
   22.21  lemma has_vector_derivative_transform_within:
   22.22    assumes "0 < d"
   22.23      and "x \<in> s"
    23.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Dec 19 17:03:17 2015 +0100
    23.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Dec 21 21:34:14 2015 +0100
    23.3 @@ -8,11 +8,12 @@
    23.4  
    23.5  theory Topology_Euclidean_Space
    23.6  imports
    23.7 -  Complex_Main
    23.8 +  "~~/src/HOL/Library/Indicator_Function"
    23.9    "~~/src/HOL/Library/Countable_Set"
   23.10    "~~/src/HOL/Library/FuncSet"
   23.11    Linear_Algebra
   23.12    Norm_Arith
   23.13 +  
   23.14  begin
   23.15  
   23.16  lemma image_affinity_interval:
   23.17 @@ -5736,6 +5737,60 @@
   23.18      done
   23.19  qed
   23.20  
   23.21 +lemma isCont_indicator: 
   23.22 +  fixes x :: "'a::t2_space"
   23.23 +  shows "isCont (indicator A :: 'a \<Rightarrow> real) x = (x \<notin> frontier A)"
   23.24 +proof auto
   23.25 +  fix x
   23.26 +  assume cts_at: "isCont (indicator A :: 'a \<Rightarrow> real) x" and fr: "x \<in> frontier A"
   23.27 +  with continuous_at_open have 1: "\<forall>V::real set. open V \<and> indicator A x \<in> V \<longrightarrow>
   23.28 +    (\<exists>U::'a set. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> V))" by auto
   23.29 +  show False
   23.30 +  proof (cases "x \<in> A")
   23.31 +    assume x: "x \<in> A"
   23.32 +    hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
   23.33 +    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
   23.34 +      using 1 open_greaterThanLessThan by blast
   23.35 +    then guess U .. note U = this
   23.36 +    hence "\<forall>y\<in>U. indicator A y > (0::real)"
   23.37 +      unfolding greaterThanLessThan_def by auto
   23.38 +    hence "U \<subseteq> A" using indicator_eq_0_iff by force
   23.39 +    hence "x \<in> interior A" using U interiorI by auto
   23.40 +    thus ?thesis using fr unfolding frontier_def by simp
   23.41 +  next
   23.42 +    assume x: "x \<notin> A"
   23.43 +    hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
   23.44 +    hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
   23.45 +      using 1 open_greaterThanLessThan by blast
   23.46 +    then guess U .. note U = this
   23.47 +    hence "\<forall>y\<in>U. indicator A y < (1::real)"
   23.48 +      unfolding greaterThanLessThan_def by auto
   23.49 +    hence "U \<subseteq> -A" by auto
   23.50 +    hence "x \<in> interior (-A)" using U interiorI by auto
   23.51 +    thus ?thesis using fr interior_complement unfolding frontier_def by auto
   23.52 +  qed
   23.53 +next
   23.54 +  assume nfr: "x \<notin> frontier A"
   23.55 +  hence "x \<in> interior A \<or> x \<in> interior (-A)"
   23.56 +    by (auto simp: frontier_def closure_interior)
   23.57 +  thus "isCont ((indicator A)::'a \<Rightarrow> real) x"
   23.58 +  proof
   23.59 +    assume int: "x \<in> interior A"
   23.60 +    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> A" unfolding interior_def by auto
   23.61 +    then guess U .. note U = this
   23.62 +    hence "\<forall>y\<in>U. indicator A y = (1::real)" unfolding indicator_def by auto
   23.63 +    hence "continuous_on U (indicator A)" by (simp add: continuous_on_const indicator_eq_1_iff)
   23.64 +    thus ?thesis using U continuous_on_eq_continuous_at by auto
   23.65 +  next
   23.66 +    assume ext: "x \<in> interior (-A)"
   23.67 +    hence "\<exists>U. open U \<and> x \<in> U \<and> U \<subseteq> -A" unfolding interior_def by auto
   23.68 +    then guess U .. note U = this
   23.69 +    hence "\<forall>y\<in>U. indicator A y = (0::real)" unfolding indicator_def by auto
   23.70 +    hence "continuous_on U (indicator A)" by (smt U continuous_on_topological indicator_def)
   23.71 +    thus ?thesis using U continuous_on_eq_continuous_at by auto
   23.72 +  qed
   23.73 +qed
   23.74 +
   23.75  text \<open>Making a continuous function avoid some value in a neighbourhood.\<close>
   23.76  
   23.77  lemma continuous_within_avoid:
    24.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Sat Dec 19 17:03:17 2015 +0100
    24.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Mon Dec 21 21:34:14 2015 +0100
    24.3 @@ -904,6 +904,12 @@
    24.4  translations
    24.5    "\<integral> x. f \<partial>M" == "CONST lebesgue_integral M (\<lambda>x. f)"
    24.6  
    24.7 +syntax
    24.8 +  "_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real" ("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
    24.9 +
   24.10 +translations
   24.11 +  "LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
   24.12 +
   24.13  lemma has_bochner_integral_integral_eq: "has_bochner_integral M f x \<Longrightarrow> integral\<^sup>L M f = x"
   24.14    by (metis the_equality has_bochner_integral_eq lebesgue_integral_def)
   24.15  
   24.16 @@ -2581,6 +2587,33 @@
   24.17      by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap[symmetric])
   24.18  qed
   24.19  
   24.20 +lemma (in pair_sigma_finite) Fubini_integrable:
   24.21 +  fixes f :: "_ \<Rightarrow> _::{banach, second_countable_topology}"
   24.22 +  assumes f[measurable]: "f \<in> borel_measurable (M1 \<Otimes>\<^sub>M M2)"
   24.23 +    and integ1: "integrable M1 (\<lambda>x. \<integral> y. norm (f (x, y)) \<partial>M2)"
   24.24 +    and integ2: "AE x in M1. integrable M2 (\<lambda>y. f (x, y))"
   24.25 +  shows "integrable (M1 \<Otimes>\<^sub>M M2) f"
   24.26 +proof (rule integrableI_bounded)
   24.27 +  have "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) = (\<integral>\<^sup>+ x. (\<integral>\<^sup>+ y. norm (f (x, y)) \<partial>M2) \<partial>M1)"
   24.28 +    by (simp add: M2.nn_integral_fst [symmetric])
   24.29 +  also have "\<dots> = (\<integral>\<^sup>+ x. \<bar>\<integral>y. norm (f (x, y)) \<partial>M2\<bar> \<partial>M1)"
   24.30 +    apply (intro nn_integral_cong_AE)
   24.31 +    using integ2
   24.32 +  proof eventually_elim
   24.33 +    fix x assume "integrable M2 (\<lambda>y. f (x, y))"
   24.34 +    then have f: "integrable M2 (\<lambda>y. norm (f (x, y)))"
   24.35 +      by simp
   24.36 +    then have "(\<integral>\<^sup>+y. ereal (norm (f (x, y))) \<partial>M2) = ereal (LINT y|M2. norm (f (x, y)))"
   24.37 +      by (rule nn_integral_eq_integral) simp
   24.38 +    also have "\<dots> = ereal \<bar>LINT y|M2. norm (f (x, y))\<bar>"
   24.39 +      using f by (auto intro!: abs_of_nonneg[symmetric] integral_nonneg_AE)
   24.40 +    finally show "(\<integral>\<^sup>+y. ereal (norm (f (x, y))) \<partial>M2) = ereal \<bar>LINT y|M2. norm (f (x, y))\<bar>" .
   24.41 +  qed
   24.42 +  also have "\<dots> < \<infinity>"
   24.43 +    using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
   24.44 +  finally show "(\<integral>\<^sup>+ p. norm (f p) \<partial>(M1 \<Otimes>\<^sub>M M2)) < \<infinity>" .
   24.45 +qed fact
   24.46 +
   24.47  lemma (in pair_sigma_finite) emeasure_pair_measure_finite:
   24.48    assumes A: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" and finite: "emeasure (M1 \<Otimes>\<^sub>M M2) A < \<infinity>"
   24.49    shows "AE x in M1. emeasure M2 {y\<in>space M2. (x, y) \<in> A} < \<infinity>"
    25.1 --- a/src/HOL/Probability/Borel_Space.thy	Sat Dec 19 17:03:17 2015 +0100
    25.2 +++ b/src/HOL/Probability/Borel_Space.thy	Mon Dec 21 21:34:14 2015 +0100
    25.3 @@ -1467,6 +1467,35 @@
    25.4      by simp
    25.5  qed
    25.6  
    25.7 +lemma is_real_interval:
    25.8 +  assumes S: "is_interval S"
    25.9 +  shows "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or> S = {a<..} \<or> S = {a..} \<or>
   25.10 +    S = {a<..<b} \<or> S = {a<..b} \<or> S = {a..<b} \<or> S = {a..b}"
   25.11 +  using S unfolding is_interval_1 by (blast intro: interval_cases)
   25.12 +
   25.13 +lemma real_interval_borel_measurable:
   25.14 +  assumes "is_interval (S::real set)"
   25.15 +  shows "S \<in> sets borel"
   25.16 +proof -
   25.17 +  from assms is_real_interval have "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or>
   25.18 +    S = {a<..} \<or> S = {a..} \<or> S = {a<..<b} \<or> S = {a<..b} \<or> S = {a..<b} \<or> S = {a..b}" by auto
   25.19 +  then guess a ..
   25.20 +  then guess b ..
   25.21 +  thus ?thesis
   25.22 +    by auto
   25.23 +qed
   25.24 +
   25.25 +lemma borel_measurable_mono:
   25.26 +  fixes f :: "real \<Rightarrow> real"
   25.27 +  assumes "mono f"
   25.28 +  shows "f \<in> borel_measurable borel"
   25.29 +proof (subst borel_measurable_iff_ge, auto simp add:)
   25.30 +  fix a :: real
   25.31 +  have "is_interval {w. a \<le> f w}"
   25.32 +    unfolding is_interval_1 using assms by (auto dest: monoD intro: order.trans)
   25.33 +  thus "{w. a \<le> f w} \<in> sets borel" using real_interval_borel_measurable by auto  
   25.34 +qed
   25.35 +
   25.36  no_notation
   25.37    eucl_less (infix "<e" 50)
   25.38  
    26.1 --- a/src/HOL/Probability/Giry_Monad.thy	Sat Dec 19 17:03:17 2015 +0100
    26.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Mon Dec 21 21:34:14 2015 +0100
    26.3 @@ -91,9 +91,9 @@
    26.4    from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
    26.5    from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on)
    26.6    from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0"
    26.7 -    by (rule mono_on_imp_deriv_nonneg) (auto simp: interior_atLeastAtMost_real)
    26.8 +    by (rule mono_on_imp_deriv_nonneg) auto
    26.9    from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
   26.10 -    by (rule continuous_ge_on_Iii) (simp_all add: \<open>a < b\<close>)
   26.11 +    by (rule continuous_ge_on_Ioo) (simp_all add: \<open>a < b\<close>)
   26.12  
   26.13    from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
   26.14    have A: "h -` {a..b} = {g a..g b}"
    27.1 --- a/src/HOL/Probability/Interval_Integral.thy	Sat Dec 19 17:03:17 2015 +0100
    27.2 +++ b/src/HOL/Probability/Interval_Integral.thy	Mon Dec 21 21:34:14 2015 +0100
    27.3 @@ -389,11 +389,11 @@
    27.4             simp add: interval_lebesgue_integral_def einterval_iff)
    27.5  
    27.6  lemma interval_integral_Ioi:
    27.7 -  "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real a <..}. f x)"
    27.8 +  "\<bar>a\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..\<infinity>. f x) = (LBINT x : {real_of_ereal a <..}. f x)"
    27.9    by (auto simp add: interval_lebesgue_integral_def einterval_iff)
   27.10  
   27.11  lemma interval_integral_Ioo:
   27.12 -  "a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real a <..< real b}. f x)"
   27.13 +  "a \<le> b \<Longrightarrow> \<bar>a\<bar> < \<infinity> ==> \<bar>b\<bar> < \<infinity> \<Longrightarrow> (LBINT x=a..b. f x) = (LBINT x : {real_of_ereal a <..< real_of_ereal b}. f x)"
   27.14    by (auto simp add: interval_lebesgue_integral_def einterval_iff)
   27.15  
   27.16  lemma interval_integral_discrete_difference:
    28.1 --- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Sat Dec 19 17:03:17 2015 +0100
    28.2 +++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Mon Dec 21 21:34:14 2015 +0100
    28.3 @@ -16,65 +16,6 @@
    28.4      "\<lbrakk>f \<in> measurable borel M; A \<in> sets M\<rbrakk> \<Longrightarrow> f -` A \<in> sets borel"
    28.5    by (drule (1) measurable_sets) simp
    28.6  
    28.7 -lemma closure_Iii: 
    28.8 -  assumes "a < b"
    28.9 -  shows "closure {a<..<b::real} = {a..b}"
   28.10 -proof-
   28.11 -  have "{a<..<b} = ball ((a+b)/2) ((b-a)/2)" by (auto simp: dist_real_def field_simps not_less)
   28.12 -  also from assms have "closure ... = cball ((a+b)/2) ((b-a)/2)" by (intro closure_ball) simp
   28.13 -  also have "... = {a..b}" by (auto simp: dist_real_def field_simps not_less)
   28.14 -  finally show ?thesis .
   28.15 -qed
   28.16 -
   28.17 -lemma continuous_ge_on_Iii:
   28.18 -  assumes "continuous_on {c..d} g" "\<And>x. x \<in> {c<..<d} \<Longrightarrow> g x \<ge> a" "c < d" "x \<in> {c..d}"
   28.19 -  shows "g (x::real) \<ge> (a::real)"
   28.20 -proof-
   28.21 -  from assms(3) have "{c..d} = closure {c<..<d}" by (rule closure_Iii[symmetric])
   28.22 -  also from assms(2) have "{c<..<d} \<subseteq> (g -` {a..} \<inter> {c..d})" by auto
   28.23 -  hence "closure {c<..<d} \<subseteq> closure (g -` {a..} \<inter> {c..d})" by (rule closure_mono)
   28.24 -  also from assms(1) have "closed (g -` {a..} \<inter> {c..d})"
   28.25 -    by (auto simp: continuous_on_closed_vimage)
   28.26 -  hence "closure (g -` {a..} \<inter> {c..d}) = g -` {a..} \<inter> {c..d}" by simp
   28.27 -  finally show ?thesis using \<open>x \<in> {c..d}\<close> by auto 
   28.28 -qed 
   28.29 -
   28.30 -lemma interior_real_semiline':
   28.31 -  fixes a :: real
   28.32 -  shows "interior {..a} = {..<a}"
   28.33 -proof -
   28.34 -  {
   28.35 -    fix y
   28.36 -    assume "a > y"
   28.37 -    then have "y \<in> interior {..a}"
   28.38 -      apply (simp add: mem_interior)
   28.39 -      apply (rule_tac x="(a-y)" in exI)
   28.40 -      apply (auto simp add: dist_norm)
   28.41 -      done
   28.42 -  }
   28.43 -  moreover
   28.44 -  {
   28.45 -    fix y
   28.46 -    assume "y \<in> interior {..a}"
   28.47 -    then obtain e where e: "e > 0" "cball y e \<subseteq> {..a}"
   28.48 -      using mem_interior_cball[of y "{..a}"] by auto
   28.49 -    moreover from e have "y + e \<in> cball y e"
   28.50 -      by (auto simp add: cball_def dist_norm)
   28.51 -    ultimately have "a \<ge> y + e" by auto
   28.52 -    then have "a > y" using e by auto
   28.53 -  }
   28.54 -  ultimately show ?thesis by auto
   28.55 -qed
   28.56 -
   28.57 -lemma interior_atLeastAtMost_real: "interior {a..b} = {a<..<b :: real}"
   28.58 -proof-
   28.59 -  have "{a..b} = {a..} \<inter> {..b}" by auto
   28.60 -  also have "interior ... = {a<..} \<inter> {..<b}" 
   28.61 -    by (simp add: interior_real_semiline interior_real_semiline')
   28.62 -  also have "... = {a<..<b}" by auto
   28.63 -  finally show ?thesis .
   28.64 -qed
   28.65 -
   28.66  lemma nn_integral_indicator_singleton[simp]:
   28.67    assumes [measurable]: "{y} \<in> sets M"
   28.68    shows "(\<integral>\<^sup>+x. f x * indicator {y} x \<partial>M) = max 0 (f y) * emeasure M {y}"
    29.1 --- a/src/HOL/Probability/Measure_Space.thy	Sat Dec 19 17:03:17 2015 +0100
    29.2 +++ b/src/HOL/Probability/Measure_Space.thy	Mon Dec 21 21:34:14 2015 +0100
    29.3 @@ -1410,6 +1410,9 @@
    29.4  lemma measure_nonneg: "0 \<le> measure M A"
    29.5    using emeasure_nonneg[of M A] unfolding measure_def by (auto intro: real_of_ereal_pos)
    29.6  
    29.7 +lemma zero_less_measure_iff: "0 < measure M A \<longleftrightarrow> measure M A \<noteq> 0"
    29.8 +  using measure_nonneg[of M A] by (auto simp add: le_less)
    29.9 +
   29.10  lemma measure_le_0_iff: "measure M X \<le> 0 \<longleftrightarrow> measure M X = 0"
   29.11    using measure_nonneg[of M X] by auto
   29.12  
    30.1 --- a/src/HOL/Probability/Set_Integral.thy	Sat Dec 19 17:03:17 2015 +0100
    30.2 +++ b/src/HOL/Probability/Set_Integral.thy	Mon Dec 21 21:34:14 2015 +0100
    30.3 @@ -14,13 +14,6 @@
    30.4      Notation
    30.5  *)
    30.6  
    30.7 -syntax
    30.8 -"_ascii_lebesgue_integral" :: "pttrn \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
    30.9 -("(3LINT (1_)/|(_)./ _)" [0,110,60] 60)
   30.10 -
   30.11 -translations
   30.12 -"LINT x|M. f" == "CONST lebesgue_integral M (\<lambda>x. f)"
   30.13 -
   30.14  abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
   30.15  
   30.16  abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
    31.1 --- a/src/HOL/Probability/measurable.ML	Sat Dec 19 17:03:17 2015 +0100
    31.2 +++ b/src/HOL/Probability/measurable.ML	Mon Dec 21 21:34:14 2015 +0100
    31.3 @@ -204,7 +204,7 @@
    31.4  fun measurable_tac ctxt facts =
    31.5    let
    31.6      fun debug_fact msg thm () =
    31.7 -      msg ^ " " ^ Pretty.str_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
    31.8 +      msg ^ " " ^ Pretty.unformatted_string_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
    31.9  
   31.10      fun IF' c t i = COND (c i) (t i) no_tac
   31.11  
    32.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Sat Dec 19 17:03:17 2015 +0100
    32.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Dec 21 21:34:14 2015 +0100
    32.3 @@ -315,6 +315,7 @@
    32.4        | "DFG" => (DFG Monomorphic, "mono_native", liftingN)
    32.5        | _ => error ("Unknown format " ^ quote format_str ^
    32.6          " (expected \"FOF\", \"TF0\", \"TH0\", or \"DFG\")"))
    32.7 +    val generate_info = false
    32.8      val uncurried_aliases = false
    32.9      val readable_names = true
   32.10      val presimp = true
   32.11 @@ -322,7 +323,8 @@
   32.12        map (apfst (rpair (Global, Non_Rec_Def))) defs @
   32.13        map (apfst (rpair (Global, General))) nondefs
   32.14      val (atp_problem, _, _, _) =
   32.15 -      generate_atp_problem ctxt format Hypothesis (type_enc_of_string Strict type_enc) Translator
   32.16 +      generate_atp_problem ctxt generate_info format Hypothesis (type_enc_of_string Strict type_enc)
   32.17 +        Translator
   32.18          lam_trans uncurried_aliases readable_names presimp [] conj facts
   32.19  
   32.20      val ord = effective_term_order ctxt spassN
    33.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Sat Dec 19 17:03:17 2015 +0100
    33.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Dec 21 21:34:14 2015 +0100
    33.3 @@ -75,12 +75,11 @@
    33.4                  | SOME failure => string_of_atp_failure failure))
    33.5    in outcome end
    33.6  
    33.7 -fun is_problem_line_reprovable ctxt format prelude axioms deps
    33.8 -                               (Formula (ident', _, phi, _, _)) =
    33.9 +fun is_problem_line_reprovable ctxt format prelude axioms deps (Formula (ident', _, phi, _, _)) =
   33.10      is_none (run_atp ctxt format
   33.11 -        ((factsN, Formula (ident', Conjecture, phi, NONE, []) ::
   33.12 -                  map_filter (Symtab.lookup axioms) deps) ::
   33.13 -         prelude))
   33.14 +      ((factsN,
   33.15 +        Formula (ident', Conjecture, phi, NONE, []) :: map_filter (Symtab.lookup axioms) deps) ::
   33.16 +       prelude))
   33.17    | is_problem_line_reprovable _ _ _ _ _ _ = false
   33.18  
   33.19  fun inference_term _ [] = NONE
   33.20 @@ -93,7 +92,7 @@
   33.21      |> SOME
   33.22  
   33.23  fun add_inferences_to_problem_line ctxt format check_infs prelude axioms infers
   33.24 -        (line as Formula ((ident, alt), Axiom, phi, NONE, tms)) =
   33.25 +      (line as Formula ((ident, alt), Axiom, phi, NONE, info)) =
   33.26      let
   33.27        val deps =
   33.28          case these (AList.lookup (op =) infers ident) of
   33.29 @@ -106,7 +105,7 @@
   33.30            else
   33.31              deps
   33.32      in
   33.33 -      Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, tms)
   33.34 +      Formula ((ident, alt), Lemma, phi, inference_term check_infs deps, info)
   33.35      end
   33.36    | add_inferences_to_problem_line _ _ _ _ _ _ line = line
   33.37  
   33.38 @@ -170,7 +169,7 @@
   33.39        facts
   33.40        |> map (fn ((_, loc), th) =>
   33.41          ((Thm.get_name_hint th, loc), th |> Thm.prop_of |> mono ? monomorphize_term ctxt))
   33.42 -      |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
   33.43 +      |> generate_atp_problem ctxt true format Axiom type_enc Exporter combsN false false true []
   33.44          @{prop False}
   33.45        |> #1 |> sort_by (heading_sort_key o fst)
   33.46      val prelude = fst (split_last problem)
   33.47 @@ -269,13 +268,13 @@
   33.48  val hol_base_name = encode_meta "HOL"
   33.49  
   33.50  fun should_generate_problem thy base_name (Formula ((_, alt), _, _, _, _)) =
   33.51 -  case try (Global_Theory.get_thm thy) alt of
   33.52 +  (case try (Global_Theory.get_thm thy) alt of
   33.53      SOME th =>
   33.54 -    (* This is a crude hack to detect theorems stated and proved by the user (as
   33.55 -       opposed to those derived by various packages). In addition, we leave out
   33.56 -       everything in "HOL" as too basic to be interesting. *)
   33.57 +    (* This is a crude hack to detect theorems stated and proved by the user (as opposed to those
   33.58 +       derived by various packages). In addition, we leave out everything in "HOL" as too basic to
   33.59 +       be interesting. *)
   33.60      Thm.legacy_get_kind th <> "" andalso base_name <> hol_base_name
   33.61 -  | NONE => false
   33.62 +  | NONE => false)
   33.63  
   33.64  (* Convention: theoryname__goalname *)
   33.65  fun problem_name_of base_name n alt =
   33.66 @@ -342,13 +341,12 @@
   33.67        | write_problem_files n seen_facts includes seen_ss
   33.68            ((base_name, fact_line :: fact_lines) :: groups) =
   33.69          let
   33.70 -          val (ident, alt, pname, sname, conj) =
   33.71 +          val (alt, pname, sname, conj) =
   33.72              (case fact_line of
   33.73                Formula ((ident, alt), _, phi, _, _) =>
   33.74 -              (ident, alt, problem_name_of base_name n (encode_meta alt),
   33.75 +              (alt, problem_name_of base_name n (encode_meta alt),
   33.76                 suggestion_name_of base_name n (encode_meta alt),
   33.77                 Formula ((ident, alt), Conjecture, phi, NONE, [])))
   33.78 -
   33.79            val fact = the (Symtab.lookup fact_tab alt)
   33.80            val fact_s = tptp_string_of_line format fact_line
   33.81          in
    34.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Sat Dec 19 17:03:17 2015 +0100
    34.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Dec 21 21:34:14 2015 +0100
    34.3 @@ -98,7 +98,7 @@
    34.4    val tptp_empty_list : string
    34.5    val dfg_individual_type : string
    34.6    val isabelle_info_prefix : string
    34.7 -  val isabelle_info : string -> int -> (string, 'a) atp_term list
    34.8 +  val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
    34.9    val extract_isabelle_status : (string, 'a) atp_term list -> string option
   34.10    val extract_isabelle_rank : (string, 'a) atp_term list -> int
   34.11    val inductionN : string
   34.12 @@ -138,6 +138,7 @@
   34.13      ('c -> 'e) -> ('a, 'b, 'c, 'd) atp_formula -> ('a, 'b, 'e, 'd) atp_formula
   34.14    val strip_atype : 'a atp_type -> 'a list * ('a atp_type list * 'a atp_type)
   34.15    val is_format_higher_order : atp_format -> bool
   34.16 +  val tptp_string_of_format : atp_format -> string
   34.17    val tptp_string_of_line : atp_format -> string atp_problem_line -> string
   34.18    val lines_of_atp_problem :
   34.19      atp_format -> term_order -> (unit -> (string * int) list)
   34.20 @@ -271,12 +272,16 @@
   34.21  val default_rank = 1000
   34.22  val default_term_order_weight = 1
   34.23  
   34.24 -(* Currently, only SPASS 3.8ds can process Isabelle metainformation. *)
   34.25 -fun isabelle_info status rank =
   34.26 -  [] |> rank <> default_rank
   34.27 -        ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
   34.28 -                       [ATerm ((string_of_int rank, []), [])]))
   34.29 -     |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
   34.30 +(* Currently, only SPASS 3.8ds and (to a lesser extent) Metis can process Isabelle
   34.31 +   metainformation. *)
   34.32 +fun isabelle_info generate_info status rank =
   34.33 +  if generate_info then
   34.34 +    [] |> rank <> default_rank
   34.35 +          ? cons (ATerm ((isabelle_info_prefix ^ rankN, []),
   34.36 +                         [ATerm ((string_of_int rank, []), [])]))
   34.37 +       |> status <> "" ? cons (ATerm ((isabelle_info_prefix ^ status, []), []))
   34.38 +  else
   34.39 +    []
   34.40  
   34.41  fun extract_isabelle_status (ATerm ((s, []), []) :: _) =
   34.42      try (unprefix isabelle_info_prefix) s
   34.43 @@ -542,13 +547,16 @@
   34.44    | tptp_string_of_line format (Sym_Decl (ident, sym, ty)) =
   34.45      tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
   34.46      " : " ^ string_of_type format ty ^ ").\n"
   34.47 -  | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, _)) =
   34.48 +  | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, info)) =
   34.49      tptp_string_of_format format ^ "(" ^ ident ^ ", " ^
   34.50      tptp_string_of_role kind ^ "," ^ "\n    (" ^
   34.51      tptp_string_of_formula format phi ^ ")" ^
   34.52      (case source of
   34.53        SOME tm => ", " ^ tptp_string_of_term format tm
   34.54 -    | NONE => "") ^
   34.55 +    | NONE => if null info then "" else ", []") ^
   34.56 +    (case info of
   34.57 +      [] => ""
   34.58 +    | tms => ", [" ^ commas (map (tptp_string_of_term format) tms) ^ "]") ^
   34.59      ")." ^ maybe_alt alt ^ "\n"
   34.60  
   34.61  fun tptp_lines format =
    35.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Dec 19 17:03:17 2015 +0100
    35.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Dec 21 21:34:14 2015 +0100
    35.3 @@ -112,9 +112,10 @@
    35.4      Proof.context -> type_enc -> string -> term list -> term list * term list
    35.5    val string_of_status : status -> string
    35.6    val factsN : string
    35.7 -  val generate_atp_problem : Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode ->
    35.8 -    string -> bool -> bool -> bool -> term list -> term -> ((string * stature) * term) list ->
    35.9 -    string atp_problem * string Symtab.table * (string * term) list * int Symtab.table
   35.10 +  val generate_atp_problem : Proof.context -> bool -> atp_format -> atp_formula_role -> type_enc ->
   35.11 +    mode -> string -> bool -> bool -> bool -> term list -> term ->
   35.12 +    ((string * stature) * term) list -> string atp_problem * string Symtab.table
   35.13 +    * (string * term) list * int Symtab.table
   35.14    val atp_problem_selection_weights : string atp_problem -> (string * real) list
   35.15    val atp_problem_term_order_info : string atp_problem -> (string * int) list
   35.16  end;
   35.17 @@ -2017,7 +2018,7 @@
   35.18  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   35.19     of monomorphization). The TPTP forbids name clashes, and some of the remote
   35.20     provers might care. *)
   35.21 -fun line_of_fact ctxt prefix encode alt freshen pos mono type_enc rank
   35.22 +fun line_of_fact ctxt generate_info prefix encode alt freshen pos mono type_enc rank
   35.23          (j, {name, stature = (_, status), role, iformula, atomic_types}) =
   35.24    Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
   35.25              encode name, alt name),
   35.26 @@ -2027,23 +2028,22 @@
   35.27                    should_guard_var_in_formula (if pos then SOME true else NONE)
   35.28             |> close_formula_universally
   35.29             |> bound_tvars type_enc true atomic_types,
   35.30 -           NONE, isabelle_info (string_of_status status) (rank j))
   35.31 +           NONE, isabelle_info generate_info (string_of_status status) (rank j))
   35.32  
   35.33 -fun lines_of_subclass type_enc sub super =
   35.34 +fun lines_of_subclass generate_info type_enc sub super =
   35.35    Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
   35.36             AConn (AImplies,
   35.37                    [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
   35.38             |> bound_tvars type_enc false [tvar_a],
   35.39 -           NONE, isabelle_info inductiveN helper_rank)
   35.40 +           NONE, isabelle_info generate_info inductiveN helper_rank)
   35.41  
   35.42 -fun lines_of_subclass_pair type_enc (sub, supers) =
   35.43 +fun lines_of_subclass_pair generate_info type_enc (sub, supers) =
   35.44    if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
   35.45 -    [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
   35.46 -                 map (`make_class) supers)]
   35.47 +    [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)]
   35.48    else
   35.49 -    map (lines_of_subclass type_enc sub) supers
   35.50 +    map (lines_of_subclass generate_info type_enc sub) supers
   35.51  
   35.52 -fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
   35.53 +fun line_of_tcon_clause generate_info type_enc (name, prems, (cl, T)) =
   35.54    if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
   35.55      Class_Memb (class_memb_prefix ^ name,
   35.56        map (fn (cls, T) => (T |> dest_TVar |> tvar_name, map (`make_class) cls)) prems,
   35.57 @@ -2053,14 +2053,12 @@
   35.58               mk_ahorn (maps (class_atoms type_enc) prems)
   35.59                        (class_atom type_enc (cl, T))
   35.60               |> bound_tvars type_enc true (snd (dest_Type T)),
   35.61 -             NONE, isabelle_info inductiveN helper_rank)
   35.62 +             NONE, isabelle_info generate_info inductiveN helper_rank)
   35.63  
   35.64 -fun line_of_conjecture ctxt mono type_enc
   35.65 -                       ({name, role, iformula, atomic_types, ...} : ifact) =
   35.66 +fun line_of_conjecture ctxt mono type_enc ({name, role, iformula, atomic_types, ...} : ifact) =
   35.67    Formula ((conjecture_prefix ^ name, ""), role,
   35.68             iformula
   35.69 -           |> formula_of_iformula ctxt mono type_enc
   35.70 -                  should_guard_var_in_formula (SOME false)
   35.71 +           |> formula_of_iformula ctxt mono type_enc should_guard_var_in_formula (SOME false)
   35.72             |> close_formula_universally
   35.73             |> bound_tvars type_enc true atomic_types, NONE, [])
   35.74  
   35.75 @@ -2230,7 +2228,7 @@
   35.76            ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
   35.77    end
   35.78  
   35.79 -fun line_of_guards_mono_type ctxt mono type_enc T =
   35.80 +fun line_of_guards_mono_type ctxt generate_info mono type_enc T =
   35.81    Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
   35.82             Axiom,
   35.83             IConst (`make_bound_var "X", T, [])
   35.84 @@ -2240,21 +2238,21 @@
   35.85                                    (SOME true)
   35.86             |> close_formula_universally
   35.87             |> bound_tvars type_enc true (atomic_types_of T),
   35.88 -           NONE, isabelle_info inductiveN helper_rank)
   35.89 +           NONE, isabelle_info generate_info inductiveN helper_rank)
   35.90  
   35.91 -fun line_of_tags_mono_type ctxt mono type_enc T =
   35.92 +fun line_of_tags_mono_type ctxt generate_info mono type_enc T =
   35.93    let val x_var = ATerm ((`make_bound_var "X", []), []) in
   35.94      Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom,
   35.95               eq_formula type_enc (atomic_types_of T) [] false
   35.96                    (tag_with_type ctxt mono type_enc NONE T x_var) x_var,
   35.97 -             NONE, isabelle_info non_rec_defN helper_rank)
   35.98 +             NONE, isabelle_info generate_info non_rec_defN helper_rank)
   35.99    end
  35.100  
  35.101 -fun lines_of_mono_types ctxt mono type_enc =
  35.102 +fun lines_of_mono_types ctxt generate_info mono type_enc =
  35.103    (case type_enc of
  35.104      Native _ => K []
  35.105 -  | Guards _ => map (line_of_guards_mono_type ctxt mono type_enc)
  35.106 -  | Tags _ => map (line_of_tags_mono_type ctxt mono type_enc))
  35.107 +  | Guards _ => map (line_of_guards_mono_type ctxt generate_info mono type_enc)
  35.108 +  | Tags _ => map (line_of_tags_mono_type ctxt generate_info mono type_enc))
  35.109  
  35.110  fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) =
  35.111    let
  35.112 @@ -2280,8 +2278,8 @@
  35.113  
  35.114  fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
  35.115  
  35.116 -fun line_of_guards_sym_decl ctxt mono type_enc n s j
  35.117 -                            (s', T_args, T, _, ary, in_conj) =
  35.118 +fun line_of_guards_sym_decl ctxt generate_info mono type_enc n s j
  35.119 +    (s', T_args, T, _, ary, in_conj) =
  35.120    let
  35.121      val thy = Proof_Context.theory_of ctxt
  35.122      val (role, maybe_negate) = honor_conj_sym_role in_conj
  35.123 @@ -2310,11 +2308,11 @@
  35.124               |> close_formula_universally
  35.125               |> bound_tvars type_enc (n > 1) (atomic_types_of T)
  35.126               |> maybe_negate,
  35.127 -             NONE, isabelle_info inductiveN helper_rank)
  35.128 +             NONE, isabelle_info generate_info inductiveN helper_rank)
  35.129    end
  35.130  
  35.131 -fun lines_of_tags_sym_decl ctxt mono type_enc n s
  35.132 -                           (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  35.133 +fun lines_of_tags_sym_decl ctxt generate_info mono type_enc n s
  35.134 +    (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  35.135    let
  35.136      val thy = Proof_Context.theory_of ctxt
  35.137      val level = level_of_type_enc type_enc
  35.138 @@ -2330,7 +2328,7 @@
  35.139      val tag_with = tag_with_type ctxt mono type_enc NONE
  35.140      fun formula c =
  35.141        [Formula ((ident, ""), role, eq (tag_with res_T c) c, NONE,
  35.142 -                isabelle_info non_rec_defN helper_rank)]
  35.143 +                isabelle_info generate_info non_rec_defN helper_rank)]
  35.144    in
  35.145      if pred_sym orelse not (should_encode_type ctxt mono level res_T) then
  35.146        []
  35.147 @@ -2355,7 +2353,7 @@
  35.148      end
  35.149    | rationalize_decls _ decls = decls
  35.150  
  35.151 -fun lines_of_sym_decls ctxt mono type_enc (s, decls) =
  35.152 +fun lines_of_sym_decls ctxt generate_info mono type_enc (s, decls) =
  35.153    (case type_enc of
  35.154      Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)]
  35.155    | Guards (_, level) =>
  35.156 @@ -2365,21 +2363,23 @@
  35.157        val n = length decls
  35.158        val decls = decls |> filter (should_encode_type ctxt mono level o result_type_of_decl)
  35.159      in
  35.160 -      (0 upto length decls - 1, decls) |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s)
  35.161 +      (0 upto length decls - 1, decls)
  35.162 +      |-> map2 (line_of_guards_sym_decl ctxt generate_info mono type_enc n s)
  35.163      end
  35.164    | Tags (_, level) =>
  35.165      if is_type_level_uniform level then
  35.166        []
  35.167      else
  35.168        let val n = length decls in
  35.169 -        (0 upto n - 1 ~~ decls) |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s)
  35.170 +        (0 upto n - 1 ~~ decls)
  35.171 +        |> maps (lines_of_tags_sym_decl ctxt generate_info mono type_enc n s)
  35.172        end)
  35.173  
  35.174 -fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
  35.175 +fun lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts sym_decl_tab =
  35.176    let
  35.177      val syms = sym_decl_tab |> Symtab.dest |> sort_by fst
  35.178 -    val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts
  35.179 -    val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
  35.180 +    val mono_lines = lines_of_mono_types ctxt generate_info mono type_enc mono_Ts
  35.181 +    val decl_lines = maps (lines_of_sym_decls ctxt generate_info mono type_enc) syms
  35.182    in mono_lines @ decl_lines end
  35.183  
  35.184  fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases
  35.185 @@ -2426,8 +2426,8 @@
  35.186  
  35.187  fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
  35.188  
  35.189 -fun do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
  35.190 -                                    base_s0 types in_conj =
  35.191 +fun do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab base_s0
  35.192 +    types in_conj =
  35.193    let
  35.194      fun do_alias ary =
  35.195        let
  35.196 @@ -2464,31 +2464,32 @@
  35.197        in
  35.198          ([tm1, tm2],
  35.199           [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role, eq |> maybe_negate, NONE,
  35.200 -            isabelle_info non_rec_defN helper_rank)])
  35.201 +            isabelle_info generate_info non_rec_defN helper_rank)])
  35.202          |> (if ary - 1 = base_ary orelse Symtab.defined sym_tab s1 then I
  35.203              else pair_append (do_alias (ary - 1)))
  35.204        end
  35.205    in do_alias end
  35.206  
  35.207 -fun uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab
  35.208 +fun uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab
  35.209          (s, {min_ary, types, in_conj, ...} : sym_info) =
  35.210    (case unprefix_and_unascii const_prefix s of
  35.211      SOME mangled_s =>
  35.212      if String.isSubstring uncurried_alias_sep mangled_s then
  35.213        let val base_s0 = mangled_s |> unmangled_invert_const in
  35.214 -        do_uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab base_s0 types
  35.215 -          in_conj min_ary
  35.216 +        do_uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab
  35.217 +          base_s0 types in_conj min_ary
  35.218        end
  35.219      else
  35.220        ([], [])
  35.221    | NONE => ([], []))
  35.222  
  35.223 -fun uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab =
  35.224 +fun uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
  35.225 +    sym_tab0 sym_tab =
  35.226    ([], [])
  35.227    |> uncurried_aliases
  35.228 -    ? Symtab.fold_rev
  35.229 -        (pair_append o uncurried_alias_lines_of_sym ctxt ctrss mono type_enc sym_tab0 sym_tab)
  35.230 -        sym_tab
  35.231 +    ? Symtab.fold_rev (pair_append
  35.232 +        o uncurried_alias_lines_of_sym ctxt generate_info ctrss mono type_enc sym_tab0 sym_tab)
  35.233 +      sym_tab
  35.234  
  35.235  val implicit_declsN = "Could-be-implicit typings"
  35.236  val explicit_declsN = "Explicit typings"
  35.237 @@ -2563,8 +2564,8 @@
  35.238  
  35.239  val app_op_and_predicator_threshold = 45
  35.240  
  35.241 -fun generate_atp_problem ctxt format prem_role type_enc mode lam_trans uncurried_aliases
  35.242 -    readable_names presimp hyp_ts concl_t facts =
  35.243 +fun generate_atp_problem ctxt generate_info format prem_role type_enc mode lam_trans
  35.244 +    uncurried_aliases readable_names presimp hyp_ts concl_t facts =
  35.245    let
  35.246      val thy = Proof_Context.theory_of ctxt
  35.247      val type_enc = type_enc |> adjust_type_enc format
  35.248 @@ -2595,7 +2596,8 @@
  35.249      val (ho_stuff, sym_tab) =
  35.250        sym_table_of_facts ctxt type_enc Min_App_Op conjs facts
  35.251      val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
  35.252 -      uncurried_alias_lines_of_sym_table ctxt ctrss mono type_enc uncurried_aliases sym_tab0 sym_tab
  35.253 +      uncurried_alias_lines_of_sym_table ctxt generate_info ctrss mono type_enc uncurried_aliases
  35.254 +        sym_tab0 sym_tab
  35.255      val (_, sym_tab) =
  35.256        (ho_stuff, sym_tab)
  35.257        |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
  35.258 @@ -2610,7 +2612,7 @@
  35.259      val sym_decl_lines =
  35.260        (conjs, helpers @ facts, uncurried_alias_eq_tms)
  35.261        |> sym_decl_table_of_facts thy type_enc sym_tab
  35.262 -      |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
  35.263 +      |> lines_of_sym_decl_table ctxt generate_info mono type_enc mono_Ts
  35.264      val datatype_decl_lines = map decl_line_of_datatype datatypes
  35.265      val decl_lines = class_decl_lines @ sym_decl_lines @ datatype_decl_lines
  35.266      val num_facts = length facts
  35.267 @@ -2618,13 +2620,14 @@
  35.268      val pos = mode <> Exporter
  35.269      val rank_of = rank_of_fact_num num_facts
  35.270      val fact_lines =
  35.271 -      map (line_of_fact ctxt fact_prefix ascii_of I freshen pos mono type_enc rank_of)
  35.272 +      map (line_of_fact ctxt generate_info fact_prefix ascii_of I freshen pos mono type_enc rank_of)
  35.273          (0 upto num_facts - 1 ~~ facts)
  35.274 -    val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs
  35.275 -    val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses
  35.276 +    val subclass_lines = maps (lines_of_subclass_pair generate_info type_enc) subclass_pairs
  35.277 +    val tcon_lines = map (line_of_tcon_clause generate_info type_enc) tcon_clauses
  35.278      val helper_lines =
  35.279        0 upto length helpers - 1 ~~ helpers
  35.280 -      |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc (K default_rank))
  35.281 +      |> map (line_of_fact ctxt generate_info helper_prefix I (K "") false true mono type_enc
  35.282 +        (K default_rank))
  35.283      val free_type_lines = lines_of_free_types type_enc (facts @ conjs)
  35.284      val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
  35.285      (* Reordering these might confuse the proof reconstruction code. *)
    36.1 --- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Dec 19 17:03:17 2015 +0100
    36.2 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Mon Dec 21 21:34:14 2015 +0100
    36.3 @@ -368,16 +368,13 @@
    36.4              in
    36.5                if null non_trivial_assms then ()
    36.6                else
    36.7 -                let
    36.8 -                  val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
    36.9 -                    Pretty.str thm_name,
   36.10 -                    Pretty.str " transfer rule found:",
   36.11 -                    Pretty.brk 1] @ 
   36.12 -                    ((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
   36.13 -                                       [Pretty.str "."])
   36.14 -                in
   36.15 -                  warning (Pretty.str_of pretty_msg)
   36.16 -                end
   36.17 +                Pretty.block ([Pretty.str "Non-trivial assumptions in ",
   36.18 +                  Pretty.str thm_name,
   36.19 +                  Pretty.str " transfer rule found:",
   36.20 +                  Pretty.brk 1] @ 
   36.21 +                  Pretty.commas (map (Syntax.pretty_term ctxt) non_trivial_assms))
   36.22 +                |> Pretty.string_of
   36.23 +                |> warning
   36.24              end
   36.25          end
   36.26    
    37.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Sat Dec 19 17:03:17 2015 +0100
    37.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Mon Dec 21 21:34:14 2015 +0100
    37.3 @@ -227,7 +227,7 @@
    37.4      *)
    37.5      val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
    37.6      val (atp_problem, _, lifted, sym_tab) =
    37.7 -      generate_atp_problem ctxt CNF Hypothesis type_enc Metis lam_trans false false false []
    37.8 +      generate_atp_problem ctxt true CNF Hypothesis type_enc Metis lam_trans false false false []
    37.9          @{prop False} props
   37.10      (*
   37.11      val _ = tracing ("ATP PROBLEM: " ^
    38.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Dec 19 17:03:17 2015 +0100
    38.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Dec 21 21:34:14 2015 +0100
    38.3 @@ -575,11 +575,6 @@
    38.4  fun dest_n_tuple 1 t = [t]
    38.5    | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op ::
    38.6  
    38.7 -type typedef_info =
    38.8 -  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string,
    38.9 -   prop_of_Rep: thm, set_name: string option, Abs_inverse: thm option,
   38.10 -   Rep_inverse: thm option}
   38.11 -
   38.12  fun typedef_info ctxt s =
   38.13    if is_frac_type ctxt (Type (s, [])) then
   38.14      SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
    39.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Dec 19 17:03:17 2015 +0100
    39.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Dec 21 21:34:14 2015 +0100
    39.3 @@ -280,9 +280,8 @@
    39.4  val maybe_quote = ATP_Util.maybe_quote
    39.5  
    39.6  fun pretty_maybe_quote keywords pretty =
    39.7 -  let val s = Pretty.str_of pretty in
    39.8 -    if maybe_quote keywords s = s then pretty else Pretty.quote pretty
    39.9 -  end
   39.10 +  let val s = Pretty.unformatted_string_of pretty
   39.11 +  in if maybe_quote keywords s = s then pretty else Pretty.quote pretty end
   39.12  
   39.13  val hashw = ATP_Util.hashw
   39.14  val hashw_string = ATP_Util.hashw_string
    40.1 --- a/src/HOL/Tools/SMT/smtlib.ML	Sat Dec 19 17:03:17 2015 +0100
    40.2 +++ b/src/HOL/Tools/SMT/smtlib.ML	Mon Dec 21 21:34:14 2015 +0100
    40.3 @@ -186,6 +186,6 @@
    40.4    | pretty_tree (S trees) =
    40.5        Pretty.enclose "(" ")" (Pretty.separate "" (map pretty_tree trees))
    40.6  
    40.7 -val str_of = Pretty.str_of o pretty_tree
    40.8 +val str_of = Pretty.unformatted_string_of o pretty_tree
    40.9  
   40.10  end;
    41.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Dec 19 17:03:17 2015 +0100
    41.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Dec 21 21:34:14 2015 +0100
    41.3 @@ -163,7 +163,8 @@
    41.4  fun fact_of_ref ctxt keywords chained css (xthm as (xref, args)) =
    41.5    let
    41.6      val ths = Attrib.eval_thms ctxt [xthm]
    41.7 -    val bracket = implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src ctxt) args)
    41.8 +    val bracket =
    41.9 +      implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src ctxt) args)
   41.10  
   41.11      fun nth_name j =
   41.12        (case xref of
    42.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sat Dec 19 17:03:17 2015 +0100
    42.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Dec 21 21:34:14 2015 +0100
    42.3 @@ -235,6 +235,7 @@
    42.4              val num_facts =
    42.5                Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
    42.6                |> Integer.min (length facts)
    42.7 +            val generate_info = (case format of DFG _ => true | _ => false)
    42.8              val strictness = if strict then Strict else Non_Strict
    42.9              val type_enc = type_enc |> choose_type_enc strictness best_type_enc format
   42.10              val sound = is_type_enc_sound type_enc
   42.11 @@ -273,8 +274,8 @@
   42.12                        generate_waldmeister_problem ctxt hyp_ts concl_t
   42.13                        #> (fn (a, b, c, d, e) => (a, b, c, d, SOME e))
   42.14                      else
   42.15 -                      generate_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
   42.16 -                        uncurried_aliases readable_names true hyp_ts concl_t
   42.17 +                      generate_atp_problem ctxt generate_info format prem_role type_enc atp_mode
   42.18 +                        lam_trans uncurried_aliases readable_names true hyp_ts concl_t
   42.19                        #> (fn (a, b, c, d) => (a, b, c, d, NONE)))
   42.20  
   42.21              fun sel_weights () = atp_problem_selection_weights atp_problem
    43.1 --- a/src/HOL/Tools/record.ML	Sat Dec 19 17:03:17 2015 +0100
    43.2 +++ b/src/HOL/Tools/record.ML	Mon Dec 21 21:34:14 2015 +0100
    43.3 @@ -1805,6 +1805,13 @@
    43.4       distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [],
    43.5       split_sels = [], split_sel_asms = [], case_eq_ifs = []};
    43.6  
    43.7 +fun lhs_of_equation (Const (@{const_name Pure.eq}, _) $ t $ _) = t
    43.8 +  | lhs_of_equation (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _)) = t;
    43.9 +
   43.10 +fun add_spec_rule rule =
   43.11 +  let val head = head_of (lhs_of_equation (Thm.prop_of rule)) in
   43.12 +    Spec_Rules.add_global Spec_Rules.Equational ([head], [rule])
   43.13 +  end;
   43.14  
   43.15  (* definition *)
   43.16  
   43.17 @@ -2040,7 +2047,7 @@
   43.18                  map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
   43.19            ||>> (Global_Theory.add_defs false o
   43.20                  map (rpair [Code.add_default_eqn_attribute]
   43.21 -                o apfst (Binding.concealed o Binding.name))) (*FIXME Spec_Rules (?)*)
   43.22 +                o apfst (Binding.concealed o Binding.name)))
   43.23              [make_spec, fields_spec, extend_spec, truncate_spec]);
   43.24      val defs_ctxt = Proof_Context.init_global defs_thy;
   43.25  
   43.26 @@ -2052,7 +2059,7 @@
   43.27  
   43.28      (*selectors*)
   43.29      val sel_conv_props =
   43.30 -       map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
   43.31 +      map (fn (c, x as Free (_, T)) => mk_sel r_rec0 (c, T) === x) named_vars_more;
   43.32  
   43.33      (*updates*)
   43.34      fun mk_upd_prop i (c, T) =
   43.35 @@ -2239,8 +2246,6 @@
   43.36          sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs'
   43.37          surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs';
   43.38  
   43.39 -    val sels = map (fst o Logic.dest_equals o Thm.prop_of) sel_defs;
   43.40 -
   43.41      val final_thy =
   43.42        thms_thy'
   43.43        |> put_record name info
   43.44 @@ -2253,6 +2258,7 @@
   43.45        |> add_fieldext (extension_name, snd extension) names
   43.46        |> add_code ext_tyco vs extT ext simps' ext_inject
   43.47        |> add_ctr_sugar (Const ext) cases_scheme' ext_inject sel_convs'
   43.48 +      |> fold add_spec_rule (sel_convs' @ upd_convs' @ derived_defs')
   43.49        |> Sign.restore_naming thy0;
   43.50  
   43.51    in final_thy end;
    44.1 --- a/src/HOL/Tools/try0.ML	Sat Dec 19 17:03:17 2015 +0100
    44.2 +++ b/src/HOL/Tools/try0.ML	Mon Dec 21 21:34:14 2015 +0100
    44.3 @@ -163,7 +163,7 @@
    44.4  
    44.5  fun string_of_xthm (xref, args) =
    44.6    Facts.string_of_ref xref ^
    44.7 -  implode (map (enclose "[" "]" o Pretty.str_of o Token.pretty_src @{context}) args);
    44.8 +  implode (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src @{context}) args);
    44.9  
   44.10  val parse_fact_refs =
   44.11    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) (Parse.xthm >> string_of_xthm));
    45.1 --- a/src/HOL/Transcendental.thy	Sat Dec 19 17:03:17 2015 +0100
    45.2 +++ b/src/HOL/Transcendental.thy	Mon Dec 21 21:34:14 2015 +0100
    45.3 @@ -4680,7 +4680,7 @@
    45.4    DERIV_arctan[THEN DERIV_chain2, derivative_intros]
    45.5    DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
    45.6  
    45.7 -lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
    45.8 +lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- (pi/2)))"
    45.9    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
   45.10       (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
   45.11             intro!: tan_monotone exI[of _ "pi/2"])
    46.1 --- a/src/Pure/General/binding.ML	Sat Dec 19 17:03:17 2015 +0100
    46.2 +++ b/src/Pure/General/binding.ML	Mon Dec 21 21:34:14 2015 +0100
    46.3 @@ -156,7 +156,7 @@
    46.4        [Pretty.str (Long_Name.implode (map #1 (prefix @ qualifier) @ [name]))]
    46.5      |> Pretty.quote;
    46.6  
    46.7 -val print = Pretty.str_of o pretty;
    46.8 +val print = Pretty.unformatted_string_of o pretty;
    46.9  
   46.10  val pp = pretty o set_pos Position.none;
   46.11  
    47.1 --- a/src/Pure/General/output.ML	Sat Dec 19 17:03:17 2015 +0100
    47.2 +++ b/src/Pure/General/output.ML	Mon Dec 21 21:34:14 2015 +0100
    47.3 @@ -10,6 +10,9 @@
    47.4    val tracing: string -> unit
    47.5    val warning: string -> unit
    47.6    val legacy_feature: string -> unit
    47.7 +  val profile_time: ('a -> 'b) -> 'a -> 'b
    47.8 +  val profile_time_thread: ('a -> 'b) -> 'a -> 'b
    47.9 +  val profile_allocations: ('a -> 'b) -> 'a -> 'b
   47.10  end;
   47.11  
   47.12  signature OUTPUT =
   47.13 @@ -131,6 +134,40 @@
   47.14  fun protocol_message props ss = ! protocol_message_fn props (map output ss);
   47.15  fun try_protocol_message props ss = protocol_message props ss handle Protocol_Message _ => ();
   47.16  
   47.17 +
   47.18 +(* profiling *)
   47.19 +
   47.20 +local
   47.21 +
   47.22 +fun output_profile title entries =
   47.23 +  let
   47.24 +    val body = entries
   47.25 +      |> sort (int_ord o apply2 fst)
   47.26 +      |> map (fn (count, name) =>
   47.27 +          let
   47.28 +            val c = string_of_int count;
   47.29 +            val prefix = replicate_string (Int.max (0, 10 - size c)) " ";
   47.30 +          in prefix ^ c ^ " " ^ name end);
   47.31 +    val total = fold (curry (op +) o fst) entries 0;
   47.32 +  in
   47.33 +    if total = 0 then ()
   47.34 +    else warning (cat_lines (title :: (body @ ["total: " ^ string_of_int total])))
   47.35 +  end;
   47.36 +
   47.37 +in
   47.38 +
   47.39 +fun profile_time f x =
   47.40 +  ML_Profiling.profile_time (output_profile "time profile:") f x;
   47.41 +
   47.42 +fun profile_time_thread f x =
   47.43 +  ML_Profiling.profile_time_thread (output_profile "time profile (this thread):") f x;
   47.44 +
   47.45 +fun profile_allocations f x =
   47.46 +  ML_Profiling.profile_allocations (output_profile "allocations profile:") f x;
   47.47 +
   47.48 +end;
   47.49 +
   47.50 +
   47.51  end;
   47.52  
   47.53  structure Basic_Output: BASIC_OUTPUT = Output;
    48.1 --- a/src/Pure/General/path.ML	Sat Dec 19 17:03:17 2015 +0100
    48.2 +++ b/src/Pure/General/path.ML	Mon Dec 21 21:34:14 2015 +0100
    48.3 @@ -171,7 +171,7 @@
    48.4    let val s = implode_path path
    48.5    in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end;
    48.6  
    48.7 -val print = Pretty.str_of o pretty;
    48.8 +val print = Pretty.unformatted_string_of o pretty;
    48.9  
   48.10  
   48.11  (* base element *)
    49.1 --- a/src/Pure/General/pretty.ML	Sat Dec 19 17:03:17 2015 +0100
    49.2 +++ b/src/Pure/General/pretty.ML	Mon Dec 21 21:34:14 2015 +0100
    49.3 @@ -12,28 +12,27 @@
    49.4  breaking information.  A "break" inserts a newline if the text until
    49.5  the next break is too long to fit on the current line.  After the newline,
    49.6  text is indented to the level of the enclosing block.  Normally, if a block
    49.7 -is broken then all enclosing blocks will also be broken.  Only "inconsistent
    49.8 -breaks" are provided.
    49.9 +is broken then all enclosing blocks will also be broken.
   49.10  
   49.11 -The stored length of a block is used in breakdist (to treat each inner block as
   49.12 +The stored length of a block is used in break_dist (to treat each inner block as
   49.13  a unit for breaking).
   49.14  *)
   49.15  
   49.16  signature PRETTY =
   49.17  sig
   49.18 -  val spaces: int -> string
   49.19    val default_indent: string -> int -> Output.output
   49.20    val add_mode: string -> (string -> int -> Output.output) -> unit
   49.21    type T
   49.22 +  val make_block: Output.output * Output.output -> bool -> int -> T list -> T
   49.23    val str: string -> T
   49.24    val brk: int -> T
   49.25 +  val brk_indent: int -> int -> T
   49.26    val fbrk: T
   49.27    val breaks: T list -> T list
   49.28    val fbreaks: T list -> T list
   49.29    val blk: int * T list -> T
   49.30    val block: T list -> T
   49.31    val strs: string list -> T
   49.32 -  val raw_markup: Output.output * Output.output -> int * T list -> T
   49.33    val markup: Markup.T -> T list -> T
   49.34    val mark: Markup.T -> T -> T
   49.35    val mark_str: Markup.T * string -> T
   49.36 @@ -67,7 +66,7 @@
   49.37    val writeln: T -> unit
   49.38    val symbolic_output: T -> Output.output
   49.39    val symbolic_string_of: T -> string
   49.40 -  val str_of: T -> string
   49.41 +  val unformatted_string_of: T -> string
   49.42    val markup_chunks: Markup.T -> T list -> T
   49.43    val chunks: T list -> T
   49.44    val chunks2: T list -> T
   49.45 @@ -81,23 +80,9 @@
   49.46  structure Pretty: PRETTY =
   49.47  struct
   49.48  
   49.49 -(** spaces **)
   49.50 -
   49.51 -local
   49.52 -  val small_spaces = Vector.tabulate (65, fn i => replicate_string i Symbol.space);
   49.53 -in
   49.54 -  fun spaces k =
   49.55 -    if k < 64 then Vector.sub (small_spaces, k)
   49.56 -    else
   49.57 -      replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
   49.58 -        Vector.sub (small_spaces, k mod 64);
   49.59 -end;
   49.60 -
   49.61 -
   49.62 -
   49.63  (** print mode operations **)
   49.64  
   49.65 -fun default_indent (_: string) = spaces;
   49.66 +fun default_indent (_: string) = Symbol.spaces;
   49.67  
   49.68  local
   49.69    val default = {indent = default_indent};
   49.70 @@ -115,7 +100,7 @@
   49.71  
   49.72  fun mode_indent x y = #indent (get_mode ()) x y;
   49.73  
   49.74 -val output_spaces = Output.output o spaces;
   49.75 +val output_spaces = Output.output o Symbol.spaces;
   49.76  val add_indent = Buffer.add o output_spaces;
   49.77  
   49.78  
   49.79 @@ -123,41 +108,51 @@
   49.80  (** printing items: compound phrases, strings, and breaks **)
   49.81  
   49.82  abstype T =
   49.83 -    Block of (Output.output * Output.output) * T list * int * int
   49.84 -      (*markup output, body, indentation, length*)
   49.85 -  | String of Output.output * int  (*text, length*)
   49.86 -  | Break of bool * int  (*mandatory flag, width if not taken*)
   49.87 +    Block of (Output.output * Output.output) * bool * int * T list * int
   49.88 +      (*markup output, consistent, indentation, body, length*)
   49.89 +  | Break of bool * int * int  (*mandatory flag, width if not taken, extra indentation if taken*)
   49.90 +  | Str of Output.output * int  (*text, length*)
   49.91  with
   49.92  
   49.93 -fun length (Block (_, _, _, len)) = len
   49.94 -  | length (String (_, len)) = len
   49.95 -  | length (Break (_, wd)) = wd;
   49.96 +fun length (Block (_, _, _, _, len)) = len
   49.97 +  | length (Break (_, wd, _)) = wd
   49.98 +  | length (Str (_, len)) = len;
   49.99 +
  49.100 +fun make_block markup consistent indent body =
  49.101 +  let
  49.102 +    fun body_length prts len =
  49.103 +      let
  49.104 +        val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
  49.105 +        val len' = Int.max (fold (Integer.add o length) line 0, len);
  49.106 +      in
  49.107 +        (case rest of
  49.108 +          Break (true, _, ind) :: rest' =>
  49.109 +            body_length (Break (false, indent + ind, 0) :: rest') len'
  49.110 +        | [] => len')
  49.111 +      end;
  49.112 +  in Block (markup, consistent, indent, body, body_length body 0) end;
  49.113 +
  49.114 +fun markup_block markup indent es =
  49.115 +  make_block (Markup.output markup) false indent es;
  49.116  
  49.117  
  49.118  
  49.119  (** derived operations to create formatting expressions **)
  49.120  
  49.121 -val str = String o Output.output_width;
  49.122 +val str = Str o Output.output_width;
  49.123  
  49.124 -fun brk wd = Break (false, wd);
  49.125 -val fbrk = Break (true, 1);
  49.126 +fun brk wd = Break (false, wd, 0);
  49.127 +fun brk_indent wd ind = Break (false, wd, ind);
  49.128 +val fbrk = Break (true, 1, 0);
  49.129  
  49.130  fun breaks prts = Library.separate (brk 1) prts;
  49.131  fun fbreaks prts = Library.separate fbrk prts;
  49.132  
  49.133 -fun raw_markup m (indent, es) =
  49.134 -  let
  49.135 -    fun sum [] k = k
  49.136 -      | sum (e :: es) k = sum es (length e + k);
  49.137 -  in Block (m, es, indent, sum es 0) end;
  49.138 -
  49.139 -fun markup_block m arg = raw_markup (Markup.output m) arg;
  49.140 -
  49.141 -val blk = markup_block Markup.empty;
  49.142 +fun blk (ind, es) = markup_block Markup.empty ind es;
  49.143  fun block prts = blk (2, prts);
  49.144  val strs = block o breaks o map str;
  49.145  
  49.146 -fun markup m prts = markup_block m (0, prts);
  49.147 +fun markup m = markup_block m 0;
  49.148  fun mark m prt = if m = Markup.empty then prt else markup m [prt];
  49.149  fun mark_str (m, s) = mark m (str s);
  49.150  fun marks_str (ms, s) = fold_rev mark ms (str s);
  49.151 @@ -195,11 +190,12 @@
  49.152  fun big_list name prts = block (fbreaks (str name :: prts));
  49.153  
  49.154  fun indent 0 prt = prt
  49.155 -  | indent n prt = blk (0, [str (spaces n), prt]);
  49.156 +  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
  49.157  
  49.158 -fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
  49.159 -  | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
  49.160 -  | unbreakable (e as String _) = e;
  49.161 +fun unbreakable (Block (m, consistent, indent, es, len)) =
  49.162 +      Block (m, consistent, indent, map unbreakable es, len)
  49.163 +  | unbreakable (Break (_, wd, _)) = Str (output_spaces wd, wd)
  49.164 +  | unbreakable (e as Str _) = e;
  49.165  
  49.166  
  49.167  
  49.168 @@ -247,15 +243,17 @@
  49.169  
  49.170  (*Add the lengths of the expressions until the next Break; if no Break then
  49.171    include "after", to account for text following this block.*)
  49.172 -fun breakdist (Break _ :: _, _) = 0
  49.173 -  | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
  49.174 -  | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
  49.175 -  | breakdist ([], after) = after;
  49.176 +fun break_dist (Break _ :: _, _) = 0
  49.177 +  | break_dist (e :: es, after) = length e + break_dist (es, after)
  49.178 +  | break_dist ([], after) = after;
  49.179 +
  49.180 +val force_break = fn Break (false, wd, ind) => Break (true, wd, ind) | e => e;
  49.181 +val force_all = map force_break;
  49.182  
  49.183  (*Search for the next break (at this or higher levels) and force it to occur.*)
  49.184 -fun forcenext [] = []
  49.185 -  | forcenext (Break _ :: es) = fbrk :: es
  49.186 -  | forcenext (e :: es) = e :: forcenext es;
  49.187 +fun force_next [] = []
  49.188 +  | force_next ((e as Break _) :: es) = force_break e :: es
  49.189 +  | force_next (e :: es) = e :: force_next es;
  49.190  
  49.191  in
  49.192  
  49.193 @@ -270,29 +268,31 @@
  49.194      fun format ([], _, _) text = text
  49.195        | format (e :: es, block as (_, blockin), after) (text as {ind, pos, nl, ...}) =
  49.196            (case e of
  49.197 -            Block ((bg, en), bes, indent, _) =>
  49.198 +            Block ((bg, en), consistent, indent, bes, blen) =>
  49.199                let
  49.200                  val pos' = pos + indent;
  49.201                  val pos'' = pos' mod emergencypos;
  49.202                  val block' =
  49.203                    if pos' < emergencypos then (ind |> add_indent indent, pos')
  49.204                    else (add_indent pos'' Buffer.empty, pos'');
  49.205 +                val d = break_dist (es, after)
  49.206 +                val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes;
  49.207                  val btext: text = text
  49.208                    |> control bg
  49.209 -                  |> format (bes, block', breakdist (es, after))
  49.210 +                  |> format (bes', block', d)
  49.211                    |> control en;
  49.212                  (*if this block was broken then force the next break*)
  49.213 -                val es' = if nl < #nl btext then forcenext es else es;
  49.214 +                val es' = if nl < #nl btext then force_next es else es;
  49.215                in format (es', block, after) btext end
  49.216 -          | Break (force, wd) =>
  49.217 +          | Break (force, wd, ind) =>
  49.218                (*no break if text to next break fits on this line
  49.219                  or if breaking would add only breakgain to space*)
  49.220                format (es, block, after)
  49.221                  (if not force andalso
  49.222 -                    pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
  49.223 -                  then text |> blanks wd  (*just insert wd blanks*)
  49.224 -                  else text |> newline |> indentation block)
  49.225 -          | String str => format (es, block, after) (string str text));
  49.226 +                    pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain)
  49.227 +                 then text |> blanks wd  (*just insert wd blanks*)
  49.228 +                 else text |> newline |> indentation block |> blanks ind)
  49.229 +          | Str str => format (es, block, after) (string str text));
  49.230    in
  49.231      #tx (format ([input], (Buffer.empty, 0), 0) empty)
  49.232    end;
  49.233 @@ -305,23 +305,23 @@
  49.234  (*symbolic markup -- no formatting*)
  49.235  fun symbolic prt =
  49.236    let
  49.237 -    fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
  49.238 -      | out (Block ((bg, en), prts, indent, _)) =
  49.239 +    fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
  49.240 +      | out (Block ((bg, en), consistent, indent, prts, _)) =
  49.241            Buffer.add bg #>
  49.242 -          Buffer.markup (Markup.block indent) (fold out prts) #>
  49.243 +          Buffer.markup (Markup.block consistent indent) (fold out prts) #>
  49.244            Buffer.add en
  49.245 -      | out (String (s, _)) = Buffer.add s
  49.246 -      | out (Break (false, wd)) =
  49.247 -          Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
  49.248 -      | out (Break (true, _)) = Buffer.add (Output.output "\n");
  49.249 +      | out (Break (false, wd, ind)) =
  49.250 +          Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
  49.251 +      | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
  49.252 +      | out (Str (s, _)) = Buffer.add s;
  49.253    in out prt Buffer.empty end;
  49.254  
  49.255  (*unformatted output*)
  49.256  fun unformatted prt =
  49.257    let
  49.258 -    fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
  49.259 -      | fmt (String (s, _)) = Buffer.add s
  49.260 -      | fmt (Break (_, wd)) = Buffer.add (output_spaces wd);
  49.261 +    fun fmt (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
  49.262 +      | fmt (Break (_, wd, _)) = Buffer.add (output_spaces wd)
  49.263 +      | fmt (Str (s, _)) = Buffer.add s;
  49.264    in fmt prt Buffer.empty end;
  49.265  
  49.266  
  49.267 @@ -343,7 +343,7 @@
  49.268  val symbolic_output = Buffer.content o symbolic;
  49.269  val symbolic_string_of = Output.escape o symbolic_output;
  49.270  
  49.271 -val str_of = Output.escape o Buffer.content o unformatted;
  49.272 +val unformatted_string_of = Output.escape o Buffer.content o unformatted;
  49.273  
  49.274  
  49.275  (* chunks *)
  49.276 @@ -376,13 +376,15 @@
  49.277  
  49.278  (** ML toplevel pretty printing **)
  49.279  
  49.280 -fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
  49.281 -  | to_ML (String s) = ML_Pretty.String s
  49.282 -  | to_ML (Break b) = ML_Pretty.Break b;
  49.283 +fun to_ML (Block (m, consistent, indent, prts, _)) =
  49.284 +      ML_Pretty.Block (m, consistent, indent, map to_ML prts)
  49.285 +  | to_ML (Break b) = ML_Pretty.Break b
  49.286 +  | to_ML (Str s) = ML_Pretty.String s;
  49.287  
  49.288 -fun from_ML (ML_Pretty.Block (m, prts, ind)) = raw_markup m (ind, map from_ML prts)
  49.289 -  | from_ML (ML_Pretty.String s) = String s
  49.290 -  | from_ML (ML_Pretty.Break b) = Break b;
  49.291 +fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
  49.292 +      make_block m consistent indent (map from_ML prts)
  49.293 +  | from_ML (ML_Pretty.Break b) = Break b
  49.294 +  | from_ML (ML_Pretty.String s) = Str s;
  49.295  
  49.296  end;
  49.297  
    50.1 --- a/src/Pure/General/pretty.scala	Sat Dec 19 17:03:17 2015 +0100
    50.2 +++ b/src/Pure/General/pretty.scala	Mon Dec 21 21:34:14 2015 +0100
    50.3 @@ -9,18 +9,26 @@
    50.4  
    50.5  object Pretty
    50.6  {
    50.7 -  /* spaces */
    50.8 +  /* XML constructors */
    50.9  
   50.10 -  val space = " "
   50.11 -
   50.12 -  private val static_spaces = space * 4000
   50.13 +  val space: XML.Body = List(XML.Text(Symbol.space))
   50.14 +  def spaces(n: Int): XML.Body =
   50.15 +    if (n == 0) Nil
   50.16 +    else if (n == 1) space
   50.17 +    else List(XML.Text(Symbol.spaces(n)))
   50.18  
   50.19 -  def spaces(k: Int): String =
   50.20 -  {
   50.21 -    require(k >= 0)
   50.22 -    if (k < static_spaces.length) static_spaces.substring(0, k)
   50.23 -    else space * k
   50.24 -  }
   50.25 +  def block(consistent: Boolean, indent: Int, body: XML.Body): XML.Tree =
   50.26 +    XML.Elem(Markup.Block(consistent, indent), body)
   50.27 +  def block(indent: Int, body: XML.Body): XML.Tree = block(false, indent, body)
   50.28 +  def block(body: XML.Body): XML.Tree = block(2, body)
   50.29 +
   50.30 +  def brk(width: Int, indent: Int = 0): XML.Tree =
   50.31 +    XML.Elem(Markup.Break(width, indent), spaces(width))
   50.32 +
   50.33 +  val fbrk: XML.Tree = XML.Text("\n")
   50.34 +
   50.35 +  val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
   50.36 +  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
   50.37  
   50.38  
   50.39    /* text metric -- standardized to width of space */
   50.40 @@ -40,150 +48,131 @@
   50.41  
   50.42    /* markup trees with physical blocks and breaks */
   50.43  
   50.44 -  def block(body: XML.Body): XML.Tree = Block(2, body)
   50.45 -
   50.46 -  object Block
   50.47 -  {
   50.48 -    def apply(i: Int, body: XML.Body): XML.Tree =
   50.49 -      XML.Elem(Markup.Block(i), body)
   50.50 +  private sealed abstract class Tree { def length: Double }
   50.51 +  private case class Block(
   50.52 +    markup: Option[(Markup, Option[XML.Body])],
   50.53 +    consistent: Boolean, indent: Int, body: List[Tree], length: Double) extends Tree
   50.54 +  private case class Break(force: Boolean, width: Int, indent: Int) extends Tree
   50.55 +  { def length: Double = width.toDouble }
   50.56 +  private case class Str(string: String, length: Double) extends Tree
   50.57  
   50.58 -    def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
   50.59 -      tree match {
   50.60 -        case XML.Elem(Markup.Block(i), body) => Some((i, body))
   50.61 -        case _ => None
   50.62 -      }
   50.63 -  }
   50.64 -
   50.65 -  object Break
   50.66 -  {
   50.67 -    def apply(w: Int): XML.Tree =
   50.68 -      XML.Elem(Markup.Break(w), List(XML.Text(spaces(w))))
   50.69 +  private val FBreak = Break(true, 1, 0)
   50.70  
   50.71 -    def unapply(tree: XML.Tree): Option[Int] =
   50.72 -      tree match {
   50.73 -        case XML.Elem(Markup.Break(w), _) => Some(w)
   50.74 -        case _ => None
   50.75 +  private def make_block(
   50.76 +      markup: Option[(Markup, Option[XML.Body])],
   50.77 +      consistent: Boolean,
   50.78 +      indent: Int,
   50.79 +      body: List[Tree]): Tree =
   50.80 +  {
   50.81 +    def body_length(prts: List[Tree], len: Double): Double =
   50.82 +    {
   50.83 +      val (line, rest) =
   50.84 +        Library.take_prefix[Tree]({ case Break(true, _, _) => false case _ => true }, prts)
   50.85 +      val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
   50.86 +      rest match {
   50.87 +        case Break(true, _, ind) :: rest1 =>
   50.88 +          body_length(Break(false, indent + ind, 0) :: rest1, len1)
   50.89 +        case Nil => len1
   50.90        }
   50.91 +    }
   50.92 +    Block(markup, consistent, indent, body, body_length(body, 0.0))
   50.93    }
   50.94  
   50.95 -  val FBreak = XML.Text("\n")
   50.96 -
   50.97 -  def item(body: XML.Body): XML.Tree =
   50.98 -    Block(2, XML.elem(Markup.BULLET, List(XML.Text(space))) :: XML.Text(space) :: body)
   50.99 -
  50.100 -  val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
  50.101 -  def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
  50.102 -
  50.103 -
  50.104 -  /* standard form */
  50.105 -
  50.106 -  def standard_form(body: XML.Body): XML.Body =
  50.107 -    body flatMap {
  50.108 -      case XML.Wrapped_Elem(markup, body1, body2) =>
  50.109 -        List(XML.Wrapped_Elem(markup, body1, standard_form(body2)))
  50.110 -      case XML.Elem(markup, body) =>
  50.111 -        if (markup.name == Markup.ITEM) List(item(standard_form(body)))
  50.112 -        else List(XML.Elem(markup, standard_form(body)))
  50.113 -      case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
  50.114 -    }
  50.115 -
  50.116  
  50.117    /* formatted output */
  50.118  
  50.119 +  private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
  50.120 +  {
  50.121 +    def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
  50.122 +    def string(s: String, len: Double): Text =
  50.123 +      copy(tx = if (s == "") tx else XML.Text(s) :: tx, pos = pos + len)
  50.124 +    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
  50.125 +    def content: XML.Body = tx.reverse
  50.126 +  }
  50.127 +
  50.128 +  private def break_dist(trees: List[Tree], after: Double): Double =
  50.129 +    trees match {
  50.130 +      case (_: Break) :: _ => 0.0
  50.131 +      case t :: ts => t.length + break_dist(ts, after)
  50.132 +      case Nil => after
  50.133 +    }
  50.134 +
  50.135 +  private def force_break(tree: Tree): Tree =
  50.136 +    tree match { case Break(false, wd, ind) => Break(true, wd, ind) case _ => tree }
  50.137 +  private def force_all(trees: List[Tree]): List[Tree] = trees.map(force_break(_))
  50.138 +
  50.139 +  private def force_next(trees: List[Tree]): List[Tree] =
  50.140 +    trees match {
  50.141 +      case Nil => Nil
  50.142 +      case (t: Break) :: ts => force_break(t) :: ts
  50.143 +      case t :: ts => t :: force_next(ts)
  50.144 +    }
  50.145 +
  50.146    private val margin_default = 76.0
  50.147  
  50.148    def formatted(input: XML.Body, margin: Double = margin_default,
  50.149      metric: Metric = Metric_Default): XML.Body =
  50.150    {
  50.151 -    sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
  50.152 -    {
  50.153 -      def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
  50.154 -      def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
  50.155 -      def blanks(wd: Int): Text = string(spaces(wd))
  50.156 -      def content: XML.Body = tx.reverse
  50.157 -    }
  50.158 -
  50.159      val breakgain = margin / 20
  50.160      val emergencypos = (margin / 2).round.toInt
  50.161  
  50.162 -    def content_length(tree: XML.Tree): Double =
  50.163 -      XML.traverse_text(List(tree))(0.0)(_ + metric(_))
  50.164 -
  50.165 -    def breakdist(trees: XML.Body, after: Double): Double =
  50.166 -      trees match {
  50.167 -        case Break(_) :: _ => 0.0
  50.168 -        case FBreak :: _ => 0.0
  50.169 -        case t :: ts => content_length(t) + breakdist(ts, after)
  50.170 -        case Nil => after
  50.171 +    def make_tree(inp: XML.Body): List[Tree] =
  50.172 +      inp flatMap {
  50.173 +        case XML.Wrapped_Elem(markup, body1, body2) =>
  50.174 +          List(make_block(Some(markup, Some(body1)), false, 0, make_tree(body2)))
  50.175 +        case XML.Elem(markup, body) =>
  50.176 +          markup match {
  50.177 +            case Markup.Block(consistent, indent) =>
  50.178 +              List(make_block(None, consistent, indent, make_tree(body)))
  50.179 +            case Markup.Break(width, indent) =>
  50.180 +              List(Break(false, width, indent))
  50.181 +            case Markup(Markup.ITEM, _) =>
  50.182 +              List(make_block(None, false, 2,
  50.183 +                make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))
  50.184 +            case _ =>
  50.185 +              List(make_block(Some((markup, None)), false, 0, make_tree(body)))
  50.186 +          }
  50.187 +        case XML.Text(text) =>
  50.188 +          Library.separate(FBreak, split_lines(text).map(s => Str(s, metric(s))))
  50.189        }
  50.190  
  50.191 -    def forcenext(trees: XML.Body): XML.Body =
  50.192 -      trees match {
  50.193 -        case Nil => Nil
  50.194 -        case FBreak :: _ => trees
  50.195 -        case Break(_) :: ts => FBreak :: ts
  50.196 -        case t :: ts => t :: forcenext(ts)
  50.197 -      }
  50.198 -
  50.199 -    def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
  50.200 +    def format(trees: List[Tree], blockin: Int, after: Double, text: Text): Text =
  50.201        trees match {
  50.202          case Nil => text
  50.203  
  50.204 -        case Block(indent, body) :: ts =>
  50.205 +        case Block(markup, consistent, indent, body, blen) :: ts =>
  50.206            val pos1 = (text.pos + indent).ceil.toInt
  50.207            val pos2 = pos1 % emergencypos
  50.208 -          val blockin1 =
  50.209 -            if (pos1 < emergencypos) pos1
  50.210 -            else pos2
  50.211 -          val btext = format(body, blockin1, breakdist(ts, after), text)
  50.212 -          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
  50.213 +          val blockin1 = if (pos1 < emergencypos) pos1 else pos2
  50.214 +          val d = break_dist(ts, after)
  50.215 +          val body1 = if (consistent && text.pos + blen > margin - d) force_all(body) else body
  50.216 +          val btext =
  50.217 +            markup match {
  50.218 +              case None => format(body1, blockin1, d, text)
  50.219 +              case Some((m, markup_body)) =>
  50.220 +                val btext0 = format(body1, blockin1, d, text.copy(tx = Nil))
  50.221 +                val elem =
  50.222 +                  markup_body match {
  50.223 +                    case None => XML.Elem(m, btext0.content)
  50.224 +                    case Some(b) => XML.Wrapped_Elem(m, b, btext0.content)
  50.225 +                  }
  50.226 +                btext0.copy(tx = elem :: text.tx)
  50.227 +            }
  50.228 +          val ts1 = if (text.nl < btext.nl) force_next(ts) else ts
  50.229            format(ts1, blockin, after, btext)
  50.230  
  50.231 -        case Break(wd) :: ts =>
  50.232 -          if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
  50.233 +        case Break(force, wd, ind) :: ts =>
  50.234 +          if (!force &&
  50.235 +              text.pos + wd <= ((margin - break_dist(ts, after)) max (blockin + breakgain)))
  50.236              format(ts, blockin, after, text.blanks(wd))
  50.237 -          else format(ts, blockin, after, text.newline.blanks(blockin))
  50.238 -        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
  50.239 +          else format(ts, blockin, after, text.newline.blanks(blockin + ind))
  50.240  
  50.241 -        case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
  50.242 -          val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
  50.243 -          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
  50.244 -          val btext1 = btext.copy(tx = XML.Wrapped_Elem(markup, body1, btext.content) :: text.tx)
  50.245 -          format(ts1, blockin, after, btext1)
  50.246 -
  50.247 -        case XML.Elem(markup, body) :: ts =>
  50.248 -          val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
  50.249 -          val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
  50.250 -          val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
  50.251 -          format(ts1, blockin, after, btext1)
  50.252 -
  50.253 -        case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
  50.254 +        case Str(s, len) :: ts => format(ts, blockin, after, text.string(s, len))
  50.255        }
  50.256 -
  50.257 -    format(standard_form(input), 0, 0.0, Text()).content
  50.258 +    format(make_tree(input), 0, 0.0, Text()).content
  50.259    }
  50.260  
  50.261    def string_of(input: XML.Body, margin: Double = margin_default,
  50.262        metric: Metric = Metric_Default): String =
  50.263      XML.content(formatted(input, margin, metric))
  50.264 -
  50.265 -
  50.266 -  /* unformatted output */
  50.267 -
  50.268 -  def unformatted(input: XML.Body): XML.Body =
  50.269 -  {
  50.270 -    def fmt(tree: XML.Tree): XML.Body =
  50.271 -      tree match {
  50.272 -        case Block(_, body) => body.flatMap(fmt)
  50.273 -        case Break(wd) => List(XML.Text(spaces(wd)))
  50.274 -        case FBreak => List(XML.Text(space))
  50.275 -        case XML.Wrapped_Elem(markup, body1, body2) =>
  50.276 -          List(XML.Wrapped_Elem(markup, body1, body2.flatMap(fmt)))
  50.277 -        case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
  50.278 -        case XML.Text(_) => List(tree)
  50.279 -      }
  50.280 -    standard_form(input).flatMap(fmt)
  50.281 -  }
  50.282 -
  50.283 -  def str_of(input: XML.Body): String = XML.content(unformatted(input))
  50.284  }
    51.1 --- a/src/Pure/General/symbol.ML	Sat Dec 19 17:03:17 2015 +0100
    51.2 +++ b/src/Pure/General/symbol.ML	Mon Dec 21 21:34:14 2015 +0100
    51.3 @@ -7,6 +7,7 @@
    51.4  signature SYMBOL =
    51.5  sig
    51.6    type symbol = string
    51.7 +  val spaces: int -> string
    51.8    val STX: symbol
    51.9    val DEL: symbol
   51.10    val space: symbol
   51.11 @@ -94,6 +95,16 @@
   51.12  
   51.13  val space = chr 32;
   51.14  
   51.15 +local
   51.16 +  val small_spaces = Vector.tabulate (65, fn i => replicate_string i space);
   51.17 +in
   51.18 +  fun spaces n =
   51.19 +    if n < 64 then Vector.sub (small_spaces, n)
   51.20 +    else
   51.21 +      replicate_string (n div 64) (Vector.sub (small_spaces, 64)) ^
   51.22 +        Vector.sub (small_spaces, n mod 64);
   51.23 +end;
   51.24 +
   51.25  val comment = "\\<comment>";
   51.26  
   51.27  fun is_char s = size s = 1;
    52.1 --- a/src/Pure/General/symbol.scala	Sat Dec 19 17:03:17 2015 +0100
    52.2 +++ b/src/Pure/General/symbol.scala	Mon Dec 21 21:34:14 2015 +0100
    52.3 @@ -21,6 +21,20 @@
    52.4    type Range = Text.Range
    52.5  
    52.6  
    52.7 +  /* spaces */
    52.8 +
    52.9 +  val space = " "
   52.10 +
   52.11 +  private val static_spaces = space * 4000
   52.12 +
   52.13 +  def spaces(n: Int): String =
   52.14 +  {
   52.15 +    require(n >= 0)
   52.16 +    if (n < static_spaces.length) static_spaces.substring(0, n)
   52.17 +    else space * n
   52.18 +  }
   52.19 +
   52.20 +
   52.21    /* ASCII characters */
   52.22  
   52.23    def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
   52.24 @@ -425,7 +439,7 @@
   52.25        "\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
   52.26        "\\<Psi>", "\\<Omega>")
   52.27  
   52.28 -    val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n")
   52.29 +    val blanks = recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n")
   52.30  
   52.31      val sym_chars =
   52.32        Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
    53.1 --- a/src/Pure/General/url.ML	Sat Dec 19 17:03:17 2015 +0100
    53.2 +++ b/src/Pure/General/url.ML	Mon Dec 21 21:34:14 2015 +0100
    53.3 @@ -81,7 +81,7 @@
    53.4  
    53.5  val pretty = Pretty.mark_str o `Markup.url o implode_url;
    53.6  
    53.7 -val print = Pretty.str_of o pretty;
    53.8 +val print = Pretty.unformatted_string_of o pretty;
    53.9  
   53.10  
   53.11  (*final declarations of this structure!*)
    54.1 --- a/src/Pure/Isar/runtime.ML	Sat Dec 19 17:03:17 2015 +0100
    54.2 +++ b/src/Pure/Isar/runtime.ML	Mon Dec 21 21:34:14 2015 +0100
    54.3 @@ -76,6 +76,8 @@
    54.4          SOME exns => maps (flatten context) exns
    54.5        | NONE => [(context, identify exn)]);
    54.6  
    54.7 +val print_thy = Pretty.unformatted_string_of o Context.pretty_abbrev_thy;
    54.8 +
    54.9  in
   54.10  
   54.11  fun exn_messages_ids e =
   54.12 @@ -104,8 +106,7 @@
   54.13              | ERROR "" => "Error"
   54.14              | ERROR msg => msg
   54.15              | Fail msg => raised exn "Fail" [msg]
   54.16 -            | THEORY (msg, thys) =>
   54.17 -                raised exn "THEORY" (msg :: map (robust Context.str_of_thy) thys)
   54.18 +            | THEORY (msg, thys) => raised exn "THEORY" (msg :: map (robust print_thy) thys)
   54.19              | Ast.AST (msg, asts) =>
   54.20                  raised exn "AST" (msg :: map (robust (Pretty.string_of o Ast.pretty_ast)) asts)
   54.21              | TYPE (msg, Ts, ts) =>
    55.1 --- a/src/Pure/Isar/toplevel.ML	Sat Dec 19 17:03:17 2015 +0100
    55.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Dec 21 21:34:14 2015 +0100
    55.3 @@ -26,7 +26,6 @@
    55.4    val pretty_state: state -> Pretty.T list
    55.5    val string_of_state: state -> string
    55.6    val pretty_abstract: state -> Pretty.T
    55.7 -  val profiling: int Unsynchronized.ref
    55.8    type transition
    55.9    val empty: transition
   55.10    val name_of: transition -> string
   55.11 @@ -204,9 +203,6 @@
   55.12  
   55.13  (** toplevel transitions **)
   55.14  
   55.15 -val profiling = Unsynchronized.ref 0;
   55.16 -
   55.17 -
   55.18  (* node transactions -- maintaining stable checkpoints *)
   55.19  
   55.20  exception FAILURE of state * exn;
   55.21 @@ -568,10 +564,7 @@
   55.22    setmp_thread_position tr (fn state =>
   55.23      let
   55.24        val timing_start = Timing.start ();
   55.25 -
   55.26 -      val (result, opt_err) =
   55.27 -         state |> (apply_trans int trans |> ! profiling > 0 ? profile (! profiling));
   55.28 -
   55.29 +      val (result, opt_err) = apply_trans int trans state;
   55.30        val timing_result = Timing.result timing_start;
   55.31        val timing_props =
   55.32          Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr);
    56.1 --- a/src/Pure/ML-Systems/ml_debugger.ML	Sat Dec 19 17:03:17 2015 +0100
    56.2 +++ b/src/Pure/ML-Systems/ml_debugger.ML	Mon Dec 21 21:34:14 2015 +0100
    56.3 @@ -21,6 +21,7 @@
    56.4    val debug_function_result: state -> ML_Name_Space.valueVal
    56.5    val debug_location: state -> 'location
    56.6    val debug_name_space: state -> ML_Name_Space.T
    56.7 +  val debug_local_name_space: state -> ML_Name_Space.T
    56.8  end;
    56.9  
   56.10  structure ML_Debugger: ML_DEBUGGER =
   56.11 @@ -58,5 +59,6 @@
   56.12  fun debug_function_result () = fail ();
   56.13  fun debug_location () = fail ();
   56.14  fun debug_name_space () = fail ();
   56.15 +fun debug_local_name_space () = fail ();
   56.16  
   56.17  end;
    57.1 --- a/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML	Sat Dec 19 17:03:17 2015 +0100
    57.2 +++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.6.ML	Mon Dec 21 21:34:14 2015 +0100
    57.3 @@ -22,6 +22,7 @@
    57.4    val debug_function_result: state -> ML_Name_Space.valueVal
    57.5    val debug_location: state -> location
    57.6    val debug_name_space: state -> ML_Name_Space.T
    57.7 +  val debug_local_name_space: state -> ML_Name_Space.T
    57.8  end;
    57.9  
   57.10  structure ML_Debugger: ML_DEBUGGER =
   57.11 @@ -66,5 +67,6 @@
   57.12  val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
   57.13  val debug_location = PolyML.DebuggerInterface.debugLocation;
   57.14  val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
   57.15 +val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
   57.16  
   57.17  end;
    58.1 --- a/src/Pure/ML-Systems/ml_pretty.ML	Sat Dec 19 17:03:17 2015 +0100
    58.2 +++ b/src/Pure/ML-Systems/ml_pretty.ML	Mon Dec 21 21:34:14 2015 +0100
    58.3 @@ -8,13 +8,13 @@
    58.4  struct
    58.5  
    58.6  datatype pretty =
    58.7 -  Block of (string * string) * pretty list * int |
    58.8 +  Block of (string * string) * bool * int * pretty list |
    58.9    String of string * int |
   58.10 -  Break of bool * int;
   58.11 +  Break of bool * int * int;
   58.12  
   58.13 -fun block prts = Block (("", ""), prts, 2);
   58.14 +fun block prts = Block (("", ""), false, 2, prts);
   58.15  fun str s = String (s, size s);
   58.16 -fun brk wd = Break (false, wd);
   58.17 +fun brk width = Break (false, width, 0);
   58.18  
   58.19  fun pair pretty1 pretty2 ((x, y), depth: int) =
   58.20    block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
   58.21 @@ -28,4 +28,3 @@
   58.22    in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
   58.23  
   58.24  end;
   58.25 -
    59.1 --- a/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Sat Dec 19 17:03:17 2015 +0100
    59.2 +++ b/src/Pure/ML-Systems/ml_profiling_polyml-5.6.ML	Mon Dec 21 21:34:14 2015 +0100
    59.3 @@ -4,14 +4,16 @@
    59.4  Profiling for Poly/ML 5.6.
    59.5  *)
    59.6  
    59.7 -fun profile 0 f x = f x
    59.8 -  | profile n f x =
    59.9 -      let
   59.10 -        val mode =
   59.11 -          (case n of
   59.12 -            1 => PolyML.Profiling.ProfileTime
   59.13 -          | 2 => PolyML.Profiling.ProfileAllocations
   59.14 -          | 3 => PolyML.Profiling.ProfileLongIntEmulation
   59.15 -          | 6 => PolyML.Profiling.ProfileTimeThisThread
   59.16 -          | _ => raise Fail ("Bad profile mode: " ^ Int.toString n));
   59.17 -      in PolyML.Profiling.profile mode f x end;
   59.18 +structure ML_Profiling =
   59.19 +struct
   59.20 +
   59.21 +fun profile_time pr f x =
   59.22 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
   59.23 +
   59.24 +fun profile_time_thread pr f x =
   59.25 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
   59.26 +
   59.27 +fun profile_allocations pr f x =
   59.28 +  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
   59.29 +
   59.30 +end;
    60.1 --- a/src/Pure/ML-Systems/ml_profiling_polyml.ML	Sat Dec 19 17:03:17 2015 +0100
    60.2 +++ b/src/Pure/ML-Systems/ml_profiling_polyml.ML	Mon Dec 21 21:34:14 2015 +0100
    60.3 @@ -4,10 +4,24 @@
    60.4  Profiling for Poly/ML.
    60.5  *)
    60.6  
    60.7 -fun profile 0 f x = f x
    60.8 -  | profile n f x =
    60.9 -      let
   60.10 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   60.11 -        val res = Exn.capture f x;
   60.12 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   60.13 -      in Exn.release res end;
   60.14 +structure ML_Profiling =
   60.15 +struct
   60.16 +
   60.17 +local
   60.18 +
   60.19 +fun profile n f x =
   60.20 +  let
   60.21 +    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   60.22 +    val res = Exn.capture f x;
   60.23 +    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   60.24 +  in Exn.release res end;
   60.25 +
   60.26 +in
   60.27 +
   60.28 +fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
   60.29 +fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
   60.30 +fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
   60.31 +
   60.32 +end;
   60.33 +
   60.34 +end;
    61.1 --- a/src/Pure/ML-Systems/polyml.ML	Sat Dec 19 17:03:17 2015 +0100
    61.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Dec 21 21:34:14 2015 +0100
    61.3 @@ -132,11 +132,11 @@
    61.4  
    61.5  val pretty_ml =
    61.6    let
    61.7 -    fun convert _ (PolyML.PrettyBreak (wd, _)) = ML_Pretty.Break (false, wd)
    61.8 +    fun convert _ (PolyML.PrettyBreak (width, offset)) = ML_Pretty.Break (false, width, offset)
    61.9        | convert _ (PolyML.PrettyBlock (_, _,
   61.10              [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
   61.11 -          ML_Pretty.Break (true, 1)
   61.12 -      | convert len (PolyML.PrettyBlock (ind, _, context, prts)) =
   61.13 +          ML_Pretty.Break (true, 1, 0)
   61.14 +      | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
   61.15            let
   61.16              fun property name default =
   61.17                (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
   61.18 @@ -145,20 +145,20 @@
   61.19              val bg = property "begin" "";
   61.20              val en = property "end" "";
   61.21              val len' = property "length" len;
   61.22 -          in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
   61.23 +          in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
   61.24        | convert len (PolyML.PrettyString s) =
   61.25            ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
   61.26    in convert "" end;
   61.27  
   61.28 -fun ml_pretty (ML_Pretty.Break (false, wd)) = PolyML.PrettyBreak (wd, 0)
   61.29 -  | ml_pretty (ML_Pretty.Break (true, _)) =
   61.30 +fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
   61.31 +  | ml_pretty (ML_Pretty.Break (true, _, _)) =
   61.32        PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
   61.33          [PolyML.PrettyString " "])
   61.34 -  | ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
   61.35 +  | ml_pretty (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
   61.36        let val context =
   61.37          (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
   61.38          (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
   61.39 -      in PolyML.PrettyBlock (ind, false, context, map ml_pretty prts) end
   61.40 +      in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
   61.41    | ml_pretty (ML_Pretty.String (s, len)) =
   61.42        if len = size s then PolyML.PrettyString s
   61.43        else PolyML.PrettyBlock
    62.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sat Dec 19 17:03:17 2015 +0100
    62.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Mon Dec 21 21:34:14 2015 +0100
    62.3 @@ -74,7 +74,12 @@
    62.4    (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
    62.5  
    62.6  (*dummy implementation*)
    62.7 -fun profile (n: int) f x = f x;
    62.8 +structure ML_Profiling =
    62.9 +struct
   62.10 +  fun profile_time (_: (int * string) list -> unit) f x = f x;
   62.11 +  fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
   62.12 +  fun profile_allocations (_: (int * string) list -> unit) f x = f x;
   62.13 +end;
   62.14  
   62.15  (*dummy implementation*)
   62.16  fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
   62.17 @@ -115,12 +120,16 @@
   62.18    let
   62.19      fun str "" = ()
   62.20        | str s = PrettyPrint.string pps s;
   62.21 -    fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
   62.22 -          (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
   62.23 -            List.app pprint prts; PrettyPrint.closeBox pps; str en)
   62.24 +    fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
   62.25 +         (str bg;
   62.26 +          (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
   62.27 +            (PrettyPrint.Rel (dest_int ind));
   62.28 +          List.app pprint prts; PrettyPrint.closeBox pps;
   62.29 +          str en)
   62.30        | pprint (ML_Pretty.String (s, _)) = str s
   62.31 -      | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
   62.32 -      | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
   62.33 +      | pprint (ML_Pretty.Break (false, width, offset)) =
   62.34 +          PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
   62.35 +      | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
   62.36    in pprint end;
   62.37  
   62.38  fun toplevel_pp context path pp =
    63.1 --- a/src/Pure/PIDE/markup.ML	Sat Dec 19 17:03:17 2015 +0100
    63.2 +++ b/src/Pure/PIDE/markup.ML	Mon Dec 21 21:34:14 2015 +0100
    63.3 @@ -64,9 +64,9 @@
    63.4    val urlN: string val url: string -> T
    63.5    val docN: string val doc: string -> T
    63.6    val indentN: string
    63.7 -  val blockN: string val block: int -> T
    63.8    val widthN: string
    63.9 -  val breakN: string val break: int -> T
   63.10 +  val blockN: string val block: bool -> int -> T
   63.11 +  val breakN: string val break: int -> int -> T
   63.12    val fbreakN: string val fbreak: T
   63.13    val itemN: string val item: T
   63.14    val wordsN: string val words: T
   63.15 @@ -377,11 +377,21 @@
   63.16  
   63.17  (* pretty printing *)
   63.18  
   63.19 +val consistentN = "consistent";
   63.20  val indentN = "indent";
   63.21 -val (blockN, block) = markup_int "block" indentN;
   63.22 +val widthN = "width";
   63.23  
   63.24 -val widthN = "width";
   63.25 -val (breakN, break) = markup_int "break" widthN;
   63.26 +val blockN = "block";
   63.27 +fun block c i =
   63.28 +  (blockN,
   63.29 +    (if c then [(consistentN, print_bool c)] else []) @
   63.30 +    (if i <> 0 then [(indentN, print_int i)] else []));
   63.31 +
   63.32 +val breakN = "break";
   63.33 +fun break w i =
   63.34 +  (breakN,
   63.35 +    (if w <> 0 then [(widthN, print_int w)] else []) @
   63.36 +    (if i <> 0 then [(indentN, print_int i)] else []));
   63.37  
   63.38  val (fbreakN, fbreak) = markup_elem "fbreak";
   63.39  
    64.1 --- a/src/Pure/PIDE/markup.scala	Sat Dec 19 17:03:17 2015 +0100
    64.2 +++ b/src/Pure/PIDE/markup.scala	Mon Dec 21 21:34:14 2015 +0100
    64.3 @@ -180,8 +180,41 @@
    64.4  
    64.5    /* pretty printing */
    64.6  
    64.7 -  val Block = new Markup_Int("block", "indent")
    64.8 -  val Break = new Markup_Int("break", "width")
    64.9 +  val Consistent = new Properties.Boolean("consistent")
   64.10 +  val Indent = new Properties.Int("indent")
   64.11 +  val Width = new Properties.Int("width")
   64.12 +
   64.13 +  object Block
   64.14 +  {
   64.15 +    val name = "block"
   64.16 +    def apply(c: Boolean, i: Int): Markup =
   64.17 +      Markup(name,
   64.18 +        (if (c) Consistent(c) else Nil) :::
   64.19 +        (if (i != 0) Indent(i) else Nil))
   64.20 +    def unapply(markup: Markup): Option[(Boolean, Int)] =
   64.21 +      if (markup.name == name) {
   64.22 +        val c = Consistent.unapply(markup.properties).getOrElse(false)
   64.23 +        val i = Indent.unapply(markup.properties).getOrElse(0)
   64.24 +        Some((c, i))
   64.25 +      }
   64.26 +      else None
   64.27 +  }
   64.28 +
   64.29 +  object Break
   64.30 +  {
   64.31 +    val name = "break"
   64.32 +    def apply(w: Int, i: Int): Markup =
   64.33 +      Markup(name,
   64.34 +        (if (w != 0) Width(w) else Nil) :::
   64.35 +        (if (i != 0) Indent(i) else Nil))
   64.36 +    def unapply(markup: Markup): Option[(Int, Int)] =
   64.37 +      if (markup.name == name) {
   64.38 +        val w = Width.unapply(markup.properties).getOrElse(0)
   64.39 +        val i = Indent.unapply(markup.properties).getOrElse(0)
   64.40 +        Some((w, i))
   64.41 +      }
   64.42 +      else None
   64.43 +  }
   64.44  
   64.45    val ITEM = "item"
   64.46    val BULLET = "bullet"
    65.1 --- a/src/Pure/Proof/extraction.ML	Sat Dec 19 17:03:17 2015 +0100
    65.2 +++ b/src/Pure/Proof/extraction.ML	Mon Dec 21 21:34:14 2015 +0100
    65.3 @@ -121,7 +121,7 @@
    65.4  fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
    65.5  fun corr_name s vs = extr_name s vs ^ "_correctness";
    65.6  
    65.7 -fun msg d s = writeln (Pretty.spaces d ^ s);
    65.8 +fun msg d s = writeln (Symbol.spaces d ^ s);
    65.9  
   65.10  fun vars_of t = map Var (rev (Term.add_vars t []));
   65.11  fun frees_of t = map Free (rev (Term.add_frees t []));
    66.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Dec 19 17:03:17 2015 +0100
    66.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Mon Dec 21 21:34:14 2015 +0100
    66.3 @@ -750,7 +750,7 @@
    66.4          let
    66.5            val ((bg1, bg2), en) = typing_elem;
    66.6            val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty ty) ^ bg2;
    66.7 -        in SOME (Pretty.raw_markup (bg, en) (0, [pretty_ast Markup.empty t])) end
    66.8 +        in SOME (Pretty.make_block (bg, en) false 0 [pretty_ast Markup.empty t]) end
    66.9        else NONE
   66.10  
   66.11      and ofsort_trans ty s =
   66.12 @@ -758,7 +758,7 @@
   66.13          let
   66.14            val ((bg1, bg2), en) = sorting_elem;
   66.15            val bg = bg1 ^ Pretty.symbolic_output (pretty_typ_ast Markup.empty s) ^ bg2;
   66.16 -        in SOME (Pretty.raw_markup (bg, en) (0, [pretty_typ_ast Markup.empty ty])) end
   66.17 +        in SOME (Pretty.make_block (bg, en) false 0 [pretty_typ_ast Markup.empty ty]) end
   66.18        else NONE
   66.19  
   66.20      and pretty_typ_ast m ast = ast
    67.1 --- a/src/Pure/Thy/thy_output.ML	Sat Dec 19 17:03:17 2015 +0100
    67.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Dec 21 21:34:14 2015 +0100
    67.3 @@ -592,8 +592,9 @@
    67.4          #> space_implode "\\isasep\\isanewline%\n"
    67.5          #> Latex.environment "isabelle"
    67.6        else
    67.7 -        map ((if Config.get ctxt break then string_of_margin ctxt else Pretty.str_of) #>
    67.8 -          Output.output)
    67.9 +        map
   67.10 +          ((if Config.get ctxt break then string_of_margin ctxt else Pretty.unformatted_string_of)
   67.11 +            #> Output.output)
   67.12          #> space_implode "\\isasep\\isanewline%\n"
   67.13          #> enclose "\\isa{" "}");
   67.14  
   67.15 @@ -602,7 +603,7 @@
   67.16  
   67.17  fun verbatim_text ctxt =
   67.18    if Config.get ctxt display then
   67.19 -    split_lines #> map (prefix (Pretty.spaces (Config.get ctxt indent))) #> cat_lines #>
   67.20 +    split_lines #> map (prefix (Symbol.spaces (Config.get ctxt indent))) #> cat_lines #>
   67.21      Latex.output_ascii #> Latex.environment "isabellett"
   67.22    else
   67.23      split_lines #>
    68.1 --- a/src/Pure/Tools/debugger.ML	Sat Dec 19 17:03:17 2015 +0100
    68.2 +++ b/src/Pure/Tools/debugger.ML	Mon Dec 21 21:34:14 2015 +0100
    68.3 @@ -191,7 +191,7 @@
    68.4      fun print x =
    68.5        Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
    68.6      fun print_all () =
    68.7 -      #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) ()
    68.8 +      #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
    68.9        |> sort_by #1 |> map (Pretty.item o single o print o #2)
   68.10        |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   68.11    in Context.setmp_thread_data (SOME context) print_all () end;
    69.1 --- a/src/Pure/context.ML	Sat Dec 19 17:03:17 2015 +0100
    69.2 +++ b/src/Pure/context.ML	Mon Dec 21 21:34:14 2015 +0100
    69.3 @@ -37,9 +37,7 @@
    69.4    val theory_name: theory -> string
    69.5    val PureN: string
    69.6    val pretty_thy: theory -> Pretty.T
    69.7 -  val string_of_thy: theory -> string
    69.8    val pretty_abbrev_thy: theory -> Pretty.T
    69.9 -  val str_of_thy: theory -> string
   69.10    val get_theory: theory -> string -> theory
   69.11    val this_theory: theory -> string -> theory
   69.12    val eq_thy_id: theory_id * theory_id -> bool
   69.13 @@ -170,7 +168,6 @@
   69.14    in rev (name :: ancestor_names) end;
   69.15  
   69.16  val pretty_thy = Pretty.str_list "{" "}" o display_names;
   69.17 -val string_of_thy = Pretty.string_of o pretty_thy;
   69.18  
   69.19  fun pretty_abbrev_thy thy =
   69.20    let
   69.21 @@ -179,8 +176,6 @@
   69.22      val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   69.23    in Pretty.str_list "{" "}" abbrev end;
   69.24  
   69.25 -val str_of_thy = Pretty.str_of o pretty_abbrev_thy;
   69.26 -
   69.27  fun get_theory thy name =
   69.28    if theory_name thy <> name then
   69.29      (case find_first (fn thy' => theory_name thy' = name) (ancestors_of thy) of
    70.1 --- a/src/Pure/defs.ML	Sat Dec 19 17:03:17 2015 +0100
    70.2 +++ b/src/Pure/defs.ML	Mon Dec 21 21:34:14 2015 +0100
    70.3 @@ -147,7 +147,8 @@
    70.4  fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
    70.5    Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
    70.6      i = j orelse disjoint_args (Ts, Us) orelse
    70.7 -      error ("Clash of specifications for " ^ Pretty.str_of (pretty_item context c) ^ ":\n" ^
    70.8 +      error ("Clash of specifications for " ^
    70.9 +        Pretty.unformatted_string_of (pretty_item context c) ^ ":\n" ^
   70.10          "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
   70.11          "  " ^ quote b ^ Position.here pos_b));
   70.12  
    71.1 --- a/src/Pure/library.scala	Sat Dec 19 17:03:17 2015 +0100
    71.2 +++ b/src/Pure/library.scala	Mon Dec 21 21:34:14 2015 +0100
    71.3 @@ -205,7 +205,10 @@
    71.4      try { Some(new Regex(s)) } catch { case ERROR(_) => None }
    71.5  
    71.6  
    71.7 -  /* canonical list operations */
    71.8 +  /* lists */
    71.9 +
   71.10 +  def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
   71.11 +    (xs.takeWhile(pred), xs.dropWhile(pred))
   71.12  
   71.13    def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   71.14    def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
    72.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Dec 19 17:03:17 2015 +0100
    72.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Dec 21 21:34:14 2015 +0100
    72.3 @@ -179,7 +179,7 @@
    72.4                  val range = info.range + command_start
    72.5                  val content = command.source(info.range).replace('\n', ' ')
    72.6                  val info_text =
    72.7 -                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
    72.8 +                  Pretty.formatted(Library.separate(Pretty.fbrk, info.info), margin = 40.0)
    72.9                      .mkString
   72.10  
   72.11                  new DefaultMutableTreeNode(
    73.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 19 17:03:17 2015 +0100
    73.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 21 21:34:14 2015 +0100
    73.3 @@ -299,7 +299,7 @@
    73.4        def string_width(s: String): Double =
    73.5          painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
    73.6  
    73.7 -      val unit = string_width(Pretty.space) max 1.0
    73.8 +      val unit = string_width(Symbol.space) max 1.0
    73.9        val average = string_width("mix") / (3 * unit)
   73.10        def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
   73.11      }
    74.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 19 17:03:17 2015 +0100
    74.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Dec 21 21:34:14 2015 +0100
    74.3 @@ -506,7 +506,7 @@
    74.4    /* tooltips */
    74.5  
    74.6    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    74.7 -    Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
    74.8 +    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
    74.9  
   74.10    private def timing_threshold: Double = options.real("jedit_timing_threshold")
   74.11  
   74.12 @@ -585,7 +585,7 @@
   74.13        case tips =>
   74.14          val r = Text.Range(results.head.range.start, results.last.range.stop)
   74.15          val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   74.16 -        Some(Text.Info(r, Library.separate(Pretty.FBreak, all_tips)))
   74.17 +        Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
   74.18      }
   74.19    }
   74.20  
    75.1 --- a/src/Tools/jEdit/src/state_dockable.scala	Sat Dec 19 17:03:17 2015 +0100
    75.2 +++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Dec 21 21:34:14 2015 +0100
    75.3 @@ -108,8 +108,6 @@
    75.4        locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)
    75.5    add(controls.peer, BorderLayout.NORTH)
    75.6  
    75.7 -  override def focusOnDefaultComponent { update_button.requestFocus }
    75.8 -
    75.9  
   75.10    /* main */
   75.11