use continental paragraph style, which works better with mixture of (in)formal text;
tuned skips and indents;
tuned;

--- a/doc-src/IsarImplementation/Thy/Isar.thy	Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy	Sun Oct 17 20:25:36 2010 +0100
@@ -167,9 +167,8 @@
     ML_val {* Thm.nprems_of (#goal @{Isar.goal}) *}
     oops
 
-text {* \noindent Here we see 3 individual subgoals in the same way as
-  regular proof methods would do.
-*}
+text {* Here we see 3 individual subgoals in the same way as regular
+  proof methods would do.  *}
 
 
 section {* Proof methods *}
@@ -229,11 +228,11 @@
   \end{tabular}
   \medskip
 
-  \noindent The goal configuration consists of @{text "facts\<^sub>1"} and
-  @{text "facts\<^sub>2"} appended in that order, and various @{text "props"}
-  being claimed here.  The @{text "initial_method"} is invoked with
-  facts and goals together and refines the problem to something that
-  is handled recursively in the proof @{text "body"}.  The @{text
+  The goal configuration consists of @{text "facts\<^sub>1"} and @{text
+  "facts\<^sub>2"} appended in that order, and various @{text "props"} being
+  claimed here.  The @{text "initial_method"} is invoked with facts
+  and goals together and refines the problem to something that is
+  handled recursively in the proof @{text "body"}.  The @{text
   "terminal_method"} has another chance to finish-off any remaining
   subgoals, but it does not see the facts of the initial step.
 
@@ -249,12 +248,12 @@
   \end{tabular}
   \medskip
 
-  \noindent The @{text "method\<^sub>1"} operates on the original claim
-  together while using @{text "facts\<^sub>1"}.  Since the @{command apply}
-  command structurally resets the facts, the @{text "method\<^sub>2"} will
-  operate on the remaining goal state without facts.  The @{text
-  "method\<^sub>3"} will see again a collection of @{text "facts\<^sub>3"} that has
-  been inserted into the script explicitly.
+  The @{text "method\<^sub>1"} operates on the original claim together while
+  using @{text "facts\<^sub>1"}.  Since the @{command apply} command
+  structurally resets the facts, the @{text "method\<^sub>2"} will operate on
+  the remaining goal state without facts.  The @{text "method\<^sub>3"} will
+  see again a collection of @{text "facts\<^sub>3"} that has been inserted
+  into the script explicitly.
 
   \medskip Empirically, Isar proof methods can be categorized as
   follows.
@@ -446,12 +445,11 @@
 *}
 setup My_Simps.setup
 
-text {* \medskip\noindent This provides ML access to a list of
-  theorems in canonical declaration order via @{ML My_Simps.get}.  The
-  user can add or delete rules via the attribute @{attribute my_simp}.
-  The actual proof method is now defined as before, but we append the
-  explicit arguments and the rules from the context.
-*}
+text {* This provides ML access to a list of theorems in canonical
+  declaration order via @{ML My_Simps.get}.  The user can add or
+  delete rules via the attribute @{attribute my_simp}.  The actual
+  proof method is now defined as before, but we append the explicit
+  arguments and the rules from the context.  *}
 
 method_setup my_simp' = {*
   Attrib.thms >> (fn thms => fn ctxt =>

--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sun Oct 17 20:25:36 2010 +0100
@@ -86,13 +86,12 @@
   \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
   \end{center}
 
-  \noindent When a definitional package is finished, the auxiliary
-  context is reset to the target context.  The target now holds
-  definitions for terms and theorems that stem from the hypothetical
-  @{text "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by
-  the particular target policy (see
-  \cite[\S4--5]{Haftmann-Wenzel:2009} for details).
-*}
+  When a definitional package is finished, the auxiliary context is
+  reset to the target context.  The target now holds definitions for
+  terms and theorems that stem from the hypothetical @{text
+  "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the
+  particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
+  for details).  *}
 
 text %mlref {*
   \begin{mldecls}

--- a/doc-src/IsarImplementation/Thy/Logic.thy	Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Sun Oct 17 20:25:36 2010 +0100
@@ -286,7 +286,7 @@
   polymorphic constants that the user-level type-checker would reject
   due to violation of type class restrictions.
 
-  \medskip An \emph{atomic} term is either a variable or constant.
+  \medskip An \emph{atomic term} is either a variable or constant.
   The logical category \emph{term} is defined inductively over atomic
   terms, with abstraction and application as follows: @{text "t = b |
   x\<^isub>\<tau> | ?x\<^isub>\<tau> | c\<^isub>\<tau> | \<lambda>\<^isub>\<tau>. t | t\<^isub>1 t\<^isub>2"}.  Parsing and printing takes care of
@@ -929,9 +929,9 @@
   \end{tabular}
   \medskip
 
-  \noindent Thus we essentially impose nesting levels on propositions
-  formed from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a
-  prefix of parameters and compound premises, concluding an atomic
+  Thus we essentially impose nesting levels on propositions formed
+  from @{text "\<And>"} and @{text "\<Longrightarrow>"}.  At each level there is a prefix
+  of parameters and compound premises, concluding an atomic
   proposition.  Typical examples are @{text "\<longrightarrow>"}-introduction @{text
   "(A \<Longrightarrow> B) \<Longrightarrow> A \<longrightarrow> B"} or mathematical induction @{text "P 0 \<Longrightarrow> (\<And>n. P n
   \<Longrightarrow> P (Suc n)) \<Longrightarrow> P n"}.  Even deeper nesting occurs in well-founded

--- a/doc-src/IsarImplementation/Thy/ML.thy	Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sun Oct 17 20:25:36 2010 +0100
@@ -78,10 +78,10 @@
     | factorial n = n * factorial (n - 1)
 *}
 
-text {* \noindent Here the ML environment is really managed by
-  Isabelle, i.e.\ the @{ML factorial} function is not yet accessible
-  in the preceding paragraph, nor in a different theory that is
-  independent from the current one in the import hierarchy.
+text {* Here the ML environment is really managed by Isabelle, i.e.\
+  the @{ML factorial} function is not yet accessible in the preceding
+  paragraph, nor in a different theory that is independent from the
+  current one in the import hierarchy.
 
   Removing the above ML declaration from the source text will remove
   any trace of this definition as expected.  The Isabelle/ML toplevel
@@ -92,12 +92,11 @@
   compilation within independent nodes of the implicit theory
   development graph.}
 
-  \bigskip The next example shows how to embed ML into Isar proofs.
+  \medskip The next example shows how to embed ML into Isar proofs.
   Instead of @{command_ref "ML"} for theory mode, we use @{command_ref
   "ML_prf"} for proof mode.  As illustrated below, its effect on the
   ML environment is local to the whole proof body, while ignoring its
-  internal block structure.
-*}
+  internal block structure.  *}
 
 example_proof
   ML_prf %"ML" {* val a = 1 *}
@@ -107,20 +106,19 @@
   ML_prf %"ML" {* val c = b + 1 *}
 qed
 
-text {* \noindent By side-stepping the normal scoping rules for Isar
-  proof blocks, embedded ML code can refer to the different contexts
+text {* By side-stepping the normal scoping rules for Isar proof
+  blocks, embedded ML code can refer to the different contexts
   explicitly, and manipulate corresponding entities, e.g.\ export a
   fact from a block context.
 
-  \bigskip Two further ML commands are useful in certain situations:
+  \medskip Two further ML commands are useful in certain situations:
   @{command_ref ML_val} and @{command_ref ML_command} are both
   \emph{diagnostic} in the sense that there is no effect on the
   underlying environment, and can thus used anywhere (even outside a
   theory).  The examples below produce long strings of digits by
   invoking @{ML factorial}: @{command ML_val} already takes care of
   printing the ML toplevel result, but @{command ML_command} is silent
-  so we produce an explicit output message.
-*}
+  so we produce an explicit output message.  *}
 
 ML_val {* factorial 100 *}
 ML_command {* writeln (string_of_int (factorial 100)) *}
@@ -191,9 +189,9 @@
   ;
   \end{rail}
 
-  \noindent Here @{syntax nameref} and @{syntax args} are regular
-  outer syntax categories.  Note that attributes and proof methods use
-  similar syntax.
+  Here @{syntax nameref} and @{syntax args} are regular outer syntax
+  categories.  Note that attributes and proof methods use similar
+  syntax.
 
   \medskip A regular antiquotation @{text "@{name args}"} processes
   its arguments by the usual means of the Isar source language, and
@@ -210,9 +208,8 @@
   effect by introducing local blocks within the pre-compilation
   environment.
 
-  \bigskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader
-  perspective on Isabelle/ML antiquotations.
-*}
+  \medskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader
+  perspective on Isabelle/ML antiquotations.  *}
 
 text %mlantiq {*
   \begin{matharray}{rcl}
@@ -321,16 +318,16 @@
   perfectly legal alternative: it means that the error is absorbed
   without any message output.
 
-  \end{description}
-
-\begin{warn}
+  \begin{warn}
   The actual error channel is accessed via @{ML Output.error_msg}, but
   the interaction protocol of Proof~General \emph{crashes} if that
   function is used in regular ML code: error output and toplevel
   command failure always need to coincide here.
-\end{warn}
+  \end{warn}
 
-\begin{warn}
+  \end{description}
+
+  \begin{warn}
   Regular Isabelle/ML code should output messages exclusively by the
   official channels.  Using raw I/O on \emph{stdout} or \emph{stderr}
   instead (e.g.\ via @{ML TextIO.output}) is apt to cause problems in
@@ -340,7 +337,7 @@
   see it.  Moreover, as a genuine side-effect on global process
   channels, there is no proper way to retract output when Isar command
   transactions are reset.
-\end{warn}
+  \end{warn}
 *}
 
 

--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Oct 17 20:25:36 2010 +0100
@@ -389,9 +389,9 @@
   \end{tabular}
   \medskip
 
-  \noindent The @{text "empty"} value acts as initial default for
-  \emph{any} theory that does not declare actual data content; @{text
-  "extend"} is acts like a unitary version of @{text "merge"}.
+  The @{text "empty"} value acts as initial default for \emph{any}
+  theory that does not declare actual data content; @{text "extend"}
+  is acts like a unitary version of @{text "merge"}.
 
   Implementing @{text "merge"} can be tricky.  The general idea is
   that @{text "merge (data\<^sub>1, data\<^sub>2)"} inserts those parts of @{text
@@ -413,8 +413,8 @@
   \end{tabular}
   \medskip
 
-  \noindent The @{text "init"} operation is supposed to produce a pure
-  value from the given background theory and should be somehow
+  The @{text "init"} operation is supposed to produce a pure value
+  from the given background theory and should be somehow
   ``immediate''.  Whenever a proof context is initialized, which
   happens frequently, the the system invokes the @{text "init"}
   operation of \emph{all} theory data slots ever declared.  This also
@@ -440,13 +440,12 @@
   \end{tabular}
   \medskip
 
-  \noindent These other operations provide exclusive access for the
-  particular kind of context (theory, proof, or generic context).
-  This interface observes the ML discipline for types and scopes:
-  there is no other way to access the corresponding data slot of a
-  context.  By keeping these operations private, an Isabelle/ML module
-  may maintain abstract values authentically.
-*}
+  These other operations provide exclusive access for the particular
+  kind of context (theory, proof, or generic context).  This interface
+  observes the ML discipline for types and scopes: there is no other
+  way to access the corresponding data slot of a context.  By keeping
+  these operations private, an Isabelle/ML module may maintain
+  abstract values authentically.  *}
 
 text %mlref {*
   \begin{mldecls}
@@ -485,9 +484,9 @@
   end;
 *}
 
-text {* \noindent The implementation uses private theory data
-  internally, and only exposes an operation that involves explicit
-  argument checking wrt.\ the given theory. *}
+text {* The implementation uses private theory data internally, and
+  only exposes an operation that involves explicit argument checking
+  wrt.\ the given theory. *}
 
 ML {*
   structure Wellformed_Terms: WELLFORMED_TERMS =
@@ -500,7 +499,7 @@
     val extend = I;
     fun merge (ts1, ts2) =
       Ord_List.union Term_Ord.fast_term_ord ts1 ts2;
-  )
+  );
 
   val get = Terms.get;
 
@@ -514,11 +513,11 @@
   end;
 *}
 
-text {* \noindent We use @{ML_type "term Ord_List.T"} for reasonably
-  efficient representation of a set of terms: all operations are
-  linear in the number of stored elements.  Here we assume that users
-  of this module do not care about the declaration order, since that
-  data structure forces its own arrangement of elements.
+text {* We use @{ML_type "term Ord_List.T"} for reasonably efficient
+  representation of a set of terms: all operations are linear in the
+  number of stored elements.  Here we assume that users of this module
+  do not care about the declaration order, since that data structure
+  forces its own arrangement of elements.
 
   Observe how the @{verbatim merge} operation joins the data slots of
   the two constituents: @{ML Ord_List.union} prevents duplication of
@@ -615,13 +614,13 @@
 
   \end{enumerate}
 
-  \noindent The @{text "ident"} syntax for symbol names is @{text
-  "letter (letter | digit)\<^sup>*"}, where @{text "letter =
-  A..Za..z"} and @{text "digit = 0..9"}.  There are infinitely many
-  regular symbols and control symbols, but a fixed collection of
-  standard symbols is treated specifically.  For example,
-  ``\verb,\,\verb,<alpha>,'' is classified as a letter, which means it
-  may occur within regular Isabelle identifiers.
+  The @{text "ident"} syntax for symbol names is @{text "letter
+  (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and @{text
+  "digit = 0..9"}.  There are infinitely many regular symbols and
+  control symbols, but a fixed collection of standard symbols is
+  treated specifically.  For example, ``\verb,\,\verb,<alpha>,'' is
+  classified as a letter, which means it may occur within regular
+  Isabelle identifiers.
 
   The character set underlying Isabelle symbols is 7-bit ASCII, but
   8-bit character sequences are passed-through unchanged.  Unicode/UCS
@@ -790,7 +789,7 @@
 *}
 
 text {* \medskip The same works reletively to the formal context as
-follows. *}
+  follows. *}
 
 locale ex = fixes a b c :: 'a
 begin
@@ -843,7 +842,7 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_type indexname} \\
+  @{index_ML_type indexname: "string * int"} \\
   \end{mldecls}
 
   \begin{description}
@@ -934,13 +933,12 @@
   main equation of this ``chemical reaction'' when binding new
   entities in a context is as follows:
 
-  \smallskip
+  \medskip
   \begin{tabular}{l}
   @{text "binding + naming \<longrightarrow> long name + name space accesses"}
   \end{tabular}
-  \smallskip
 
-  \medskip As a general principle, there is a separate name space for
+  \bigskip As a general principle, there is a separate name space for
   each kind of formal entity, e.g.\ fact, logical constant, type
   constructor, type class.  It is usually clear from the occurrence in
   concrete syntax (or from the scope) which kind of entity a name
@@ -1103,16 +1101,16 @@
 
 ML {* Binding.pos_of @{binding here} *}
 
-text {* \medskip\noindent That position can be also printed in a
-  message as follows. *}
+text {* \medskip That position can be also printed in a message as
+  follows. *}
 
 ML_command {*
   writeln
     ("Look here" ^ Position.str_of (Binding.pos_of @{binding here}))
 *}
 
-text {* \noindent This illustrates a key virtue of formalized bindings
-  as opposed to raw specifications of base names: the system can use
-  this additional information for advanced feedback given to the user. *}
+text {* This illustrates a key virtue of formalized bindings as
+  opposed to raw specifications of base names: the system can use this
+  additional information for advanced feedback given to the user. *}
 
 end

--- a/doc-src/IsarImplementation/Thy/Proof.thy	Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy	Sun Oct 17 20:25:36 2010 +0100
@@ -70,9 +70,8 @@
   thm this  -- {* fully general result for arbitrary @{text "?x::?'a"} *}
 qed
 
-text {*
-  \medskip The Isabelle/Isar proof context manages the gory details of
-  term vs.\ type variables, with high-level principles for moving the
+text {* The Isabelle/Isar proof context manages the details of term
+  vs.\ type variables, with high-level principles for moving the
   frontier between fixed and schematic variables.
 
   The @{text "add_fixes"} operation explictly declares fixed
@@ -195,12 +194,11 @@
     ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
 *}
 
-text {* \noindent The following ML code can now work with the invented
-  names of @{verbatim x1}, @{verbatim x2}, @{verbatim x3}, without
-  depending on the details on the system policy for introducing these
-  variants.  Recall that within a proof body the system always invents
-  fresh ``skolem constants'', e.g.\ as follows:
-*}
+text {* The following ML code can now work with the invented names of
+  @{verbatim x1}, @{verbatim x2}, @{verbatim x3}, without depending on
+  the details on the system policy for introducing these variants.
+  Recall that within a proof body the system always invents fresh
+  ``skolem constants'', e.g.\ as follows: *}
 
 example_proof
   ML_prf %"ML" {*
@@ -215,10 +213,10 @@
   *}
   oops
 
-text {* \noindent In this situation @{ML Variable.add_fixes} and @{ML
+text {* In this situation @{ML Variable.add_fixes} and @{ML
   Variable.variant_fixes} are very similar, but identical name
   proposals given in a row are only accepted by the second version.
-*}
+  *}
 
 
 section {* Assumptions \label{sec:assumptions} *}
@@ -339,11 +337,10 @@
   val r = Assumption.export false ctxt1 ctxt0 eq';
 *}
 
-text {* \noindent Note that the variables of the resulting rule are
-  not generalized.  This would have required to fix them properly in
-  the context beforehand, and export wrt.\ variables afterwards (cf.\
-  @{ML Variable.export} or the combined @{ML "ProofContext.export"}).
-*}
+text {* Note that the variables of the resulting rule are not
+  generalized.  This would have required to fix them properly in the
+  context beforehand, and export wrt.\ variables afterwards (cf.\ @{ML
+  Variable.export} or the combined @{ML "ProofContext.export"}).  *}
 
 
 section {* Structured goals and results \label{sec:struct-goals} *}

--- a/doc-src/IsarImplementation/style.sty	Sun Oct 17 20:00:23 2010 +0100
+++ b/doc-src/IsarImplementation/style.sty	Sun Oct 17 20:25:36 2010 +0100
@@ -20,6 +20,8 @@
 \sloppy
 \binperiod
 
+\parindent 0pt\parskip 0.5ex
+
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
 \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}