redundant due to \parindent 0pt;

--- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Mon Oct 12 21:15:10 2015 +0200
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Mon Oct 12 21:42:14 2015 +0200
@@ -6,7 +6,7 @@
 begin
 
 text \<open>
-  \noindent In order to commence a new object-logic within
+  In order to commence a new object-logic within
   Isabelle/Pure we introduce abstract syntactic categories @{text "i"}
   for individuals and @{text "o"} for object-propositions.  The latter
   is embedded into the language of Pure propositions by means of a
@@ -20,7 +20,7 @@
   Trueprop :: "o \<Rightarrow> prop"    ("_" 5)
 
 text \<open>
-  \noindent Note that the object-logic judgment is implicit in the
+  Note that the object-logic judgment is implicit in the
   syntax: writing @{prop A} produces @{term "Trueprop A"} internally.
   From the Pure perspective this means ``@{prop A} is derivable in the
   object-logic''.
@@ -45,7 +45,7 @@
   subst [elim]: "x = y \<Longrightarrow> B x \<Longrightarrow> B y"
 
 text \<open>
-  \noindent Substitution is very powerful, but also hard to control in
+  Substitution is very powerful, but also hard to control in
   full generality.  We derive some common symmetry~/ transitivity
   schemes of @{term equal} as particular consequences.
 \<close>
@@ -124,7 +124,7 @@
 qed
 
 text \<open>
-  \noindent Reasoning from basic axioms is often tedious.  Our proofs
+  Reasoning from basic axioms is often tedious.  Our proofs
   work by producing various instances of the given rules (potentially
   the symmetric form) using the pattern ``@{command have}~@{text
   eq}~@{command "by"}~@{text "(rule r)"}'' and composing the chain of
@@ -157,7 +157,7 @@
 (*>*)
 
 text \<open>
-  \noindent Here we have re-used the built-in mechanism for unfolding
+  Here we have re-used the built-in mechanism for unfolding
   definitions in order to normalize each equational problem.  A more
   realistic object-logic would include proper setup for the Simplifier
   (\secref{sec:simplifier}), the main automated tool for equational
@@ -195,7 +195,7 @@
   conjD\<^sub>2: "A \<and> B \<Longrightarrow> B"
 
 text \<open>
-  \noindent The conjunctive destructions have the disadvantage that
+  The conjunctive destructions have the disadvantage that
   decomposing @{prop "A \<and> B"} involves an immediate decision which
   component should be projected.  The more convenient simultaneous
   elimination @{prop "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"} can be derived as
@@ -211,7 +211,7 @@
 qed
 
 text \<open>
-  \noindent Here is an example of swapping conjuncts with a single
+  Here is an example of swapping conjuncts with a single
   intermediate elimination step:
 \<close>
 
@@ -227,7 +227,7 @@
 (*>*)
 
 text \<open>
-  \noindent Note that the analogous elimination rule for disjunction
+  Note that the analogous elimination rule for disjunction
   ``@{text "\<ASSUMES> A \<or> B \<OBTAINS> A \<BBAR> B"}'' coincides with
   the original axiomatization of @{thm disjE}.
 
@@ -248,7 +248,7 @@
   unfolding true_def ..
 
 text \<open>
-  \medskip\noindent Now negation represents an implication towards
+  \medskip Now negation represents an implication towards
   absurdity:
 \<close>
 
@@ -312,7 +312,7 @@
 qed
 
 text \<open>
-  \noindent These examples illustrate both classical reasoning and
+  These examples illustrate both classical reasoning and
   non-trivial propositional proofs in general.  All three rules
   characterize classical logic independently, but the original rule is
   already the most convenient to use, because it leaves the conclusion
@@ -350,7 +350,7 @@
   exE [elim]: "(\<exists>x. B x) \<Longrightarrow> (\<And>x. B x \<Longrightarrow> C) \<Longrightarrow> C"
 
 text \<open>
-  \noindent The statement of @{thm exE} corresponds to ``@{text
+  The statement of @{thm exE} corresponds to ``@{text
   "\<ASSUMES> \<exists>x. B x \<OBTAINS> x \<WHERE> B x"}'' in Isar.  In the
   subsequent example we illustrate quantifier reasoning involving all
   four rules:
@@ -400,7 +400,7 @@
   \end{tabular}
   \medskip
 
-  \noindent This essentially provides a declarative reading of Pure
+  This essentially provides a declarative reading of Pure
   rules as Isar reasoning patterns: the rule statements tells how a
   canonical proof outline shall look like.  Since the above rules have
   already been declared as @{attribute (Pure) intro}, @{attribute
@@ -511,7 +511,7 @@
 (*>*)
 
 text \<open>
-  \bigskip\noindent Of course, these proofs are merely examples.  As
+  \bigskip Of course, these proofs are merely examples.  As
   sketched in \secref{sec:framework-subproof}, there is a fair amount
   of flexibility in expressing Pure deductions in Isar.  Here the user
   is asked to express himself adequately, aiming at proof texts of

--- a/src/Doc/Isar_Ref/Framework.thy	Mon Oct 12 21:15:10 2015 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy	Mon Oct 12 21:42:14 2015 +0200
@@ -97,7 +97,7 @@
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
-  \medskip\noindent Note that @{command assume} augments the proof
+  \medskip Note that @{command assume} augments the proof
   context, @{command then} indicates that the current fact shall be
   used in the next step, and @{command have} states an intermediate
   goal.  The two dots ``@{command ".."}'' refer to a complete proof of
@@ -117,7 +117,7 @@
 (*>*)
 
 text \<open>
-  \noindent The format of the @{text "\<inter>"}-introduction rule represents
+  The format of the @{text "\<inter>"}-introduction rule represents
   the most basic inference, which proceeds from given premises to a
   conclusion, without any nested proof context involved.
 
@@ -152,7 +152,7 @@
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
-  \medskip\noindent This Isar reasoning pattern again refers to the
+  \medskip This Isar reasoning pattern again refers to the
   primitive rule depicted above.  The system determines it in the
   ``@{command proof}'' step, which could have been spelled out more
   explicitly as ``@{command proof}~@{text "(rule InterI)"}''.  Note
@@ -201,7 +201,7 @@
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
-  \medskip\noindent Although the Isar proof follows the natural
+  \medskip Although the Isar proof follows the natural
   deduction rule closely, the text reads not as natural as
   anticipated.  There is a double occurrence of an arbitrary
   conclusion @{prop "C"}, which represents the final result, but is
@@ -222,7 +222,7 @@
 (*>*)
 
 text \<open>
-  \noindent Here we avoid to mention the final conclusion @{prop "C"}
+  Here we avoid to mention the final conclusion @{prop "C"}
   and return to plain forward reasoning.  The rule involved in the
   ``@{command ".."}'' proof is the same as before.
 \<close>
@@ -244,7 +244,7 @@
   \end{tabular}
   \medskip
 
-  \noindent Here only the types of syntactic terms, and the
+  Here only the types of syntactic terms, and the
   propositions of proof terms have been shown.  The @{text
   "\<lambda>"}-structure of proofs can be recorded as an optional feature of
   the Pure inference kernel @{cite "Berghofer-Nipkow:2000:TPHOL"}, but
@@ -340,7 +340,7 @@
   @{text "IntI:"}~@{prop "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B"}
   \]
 
-  \noindent This is a plain Horn clause, since no further nesting on
+  This is a plain Horn clause, since no further nesting on
   the left is involved.  The general @{text "\<Inter>"}-introduction
   corresponds to a Hereditary Harrop Formula with one additional level
   of nesting:
@@ -363,7 +363,7 @@
   \end{array}
   \]
 
-  \noindent Goal states are refined in intermediate proof steps until
+  Goal states are refined in intermediate proof steps until
   a finished form is achieved.  Here the two main reasoning principles
   are @{inference resolution}, for back-chaining a rule against a
   sub-goal (replacing it by zero or more sub-goals), and @{inference
@@ -436,7 +436,7 @@
    \end{tabular}}
   \]
 
-  \noindent Here the @{text "sub\<hyphen>proof"} rule stems from the
+  Here the @{text "sub\<hyphen>proof"} rule stems from the
   main @{command fix}-@{command assume}-@{command show} outline of
   Isar (cf.\ \secref{sec:framework-subproof}): each assumption
   indicated in the text results in a marked premise @{text "G"} above.
@@ -634,7 +634,7 @@
     \end{tabular}}
   \]
 
-  \noindent Here the name ``@{text thesis}'' is a specific convention
+  Here the name ``@{text thesis}'' is a specific convention
   for an arbitrary-but-fixed proposition; in the primitive natural
   deduction rules shown before we have occasionally used @{text C}.
   The whole statement of ``@{command obtain}~@{text x}~@{keyword
@@ -684,7 +684,7 @@
 (*>*)
 
 text \<open>
-  \bigskip\noindent This illustrates the meaning of Isar context
+  \bigskip This illustrates the meaning of Isar context
   elements without goals getting in between.
 \<close>
 
@@ -707,7 +707,7 @@
   & & \quad @{text "\<BBAR> \<dots>"} \\
   \end{tabular}
 
-  \medskip\noindent A simple @{text "statement"} consists of named
+  \medskip A simple @{text "statement"} consists of named
   propositions.  The full form admits local context elements followed
   by the actual conclusions, such as ``@{keyword "fixes"}~@{text
   x}~@{keyword "assumes"}~@{text "A x"}~@{keyword "shows"}~@{text "B
@@ -761,7 +761,7 @@
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
-  \medskip\noindent Here local facts \isacharbackquoteopen@{text "A
+  \medskip Here local facts \isacharbackquoteopen@{text "A
   x"}\isacharbackquoteclose\ and \isacharbackquoteopen@{text "B
   y"}\isacharbackquoteclose\ are referenced immediately; there is no
   need to decompose the logical rule structure again.  In the second
@@ -863,7 +863,7 @@
 text_raw \<open>\endgroup\<close>
 
 text \<open>
-  \noindent Here the @{inference refinement} inference from
+  Here the @{inference refinement} inference from
   \secref{sec:framework-resolution} mediates composition of Isar
   sub-proofs nicely.  Observe that this principle incorporates some
   degree of freedom in proof composition.  In particular, the proof
@@ -927,7 +927,7 @@
 text_raw \<open>\end{minipage}\<close>
 
 text \<open>
-  \medskip\noindent Such ``peephole optimizations'' of Isar texts are
+  \medskip Such ``peephole optimizations'' of Isar texts are
   practically important to improve readability, by rearranging
   contexts elements according to the natural flow of reasoning in the
   body, while still observing the overall scoping rules.
@@ -974,7 +974,7 @@
     @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\
   \end{matharray}
 
-  \noindent The start of a calculation is determined implicitly in the
+  The start of a calculation is determined implicitly in the
   text: here @{command also} sets @{fact calculation} to the current
   result; any subsequent occurrence will update @{fact calculation} by
   combination with the next result and a transitivity rule.  The
@@ -998,7 +998,7 @@
 (*>*)
 
 text \<open>
-  \noindent The term ``@{text "\<dots>"}'' above is a special abbreviation
+  The term ``@{text "\<dots>"}'' above is a special abbreviation
   provided by the Isabelle/Isar syntax layer: it statically refers to
   the right-hand side argument of the previous statement given in the
   text.  Thus it happens to coincide with relevant sub-expressions in

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Oct 12 21:15:10 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Oct 12 21:42:14 2015 +0200
@@ -876,7 +876,7 @@
   \end{tabular}
   \end{center}
 
-  \noindent The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
+  The ASCII representation of @{text "\<lparr>x = a\<rparr>"} is @{text
   "(| x = a |)"}.
 
   A fixed record @{text "\<lparr>x = a, y = b\<rparr>"} has field @{text x} of value
@@ -1025,7 +1025,7 @@
   \end{tabular}
   \medskip
 
-  \noindent Some further operations address the extension aspect of a
+  Some further operations address the extension aspect of a
   derived record scheme specifically: @{text "t.fields"} produces a record
   fragment consisting of exactly the new fields introduced here (the result
   may serve as a more part elsewhere); @{text "t.extend"} takes a fixed
@@ -1041,7 +1041,7 @@
   \end{tabular}
   \medskip
 
-  \noindent Note that @{text "t.make"} and @{text "t.fields"} coincide for
+  Note that @{text "t.make"} and @{text "t.fields"} coincide for
   root records.
 \<close>
 
@@ -1281,7 +1281,7 @@
       @{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<sigma>\<^sub>k \<Rightarrow> (\<^vec>\<alpha>\<^sub>n) t \<Rightarrow> (\<^vec>\<beta>\<^sub>n) t"} \\
   \end{matharray}
 
-  \noindent where @{text t} is the type constructor, @{text "\<^vec>\<alpha>\<^sub>n"}
+  where @{text t} is the type constructor, @{text "\<^vec>\<alpha>\<^sub>n"}
   and @{text "\<^vec>\<beta>\<^sub>n"} are distinct type variables free in the local
   theory and @{text "\<sigma>\<^sub>1"}, \ldots, @{text "\<sigma>\<^sub>k"} is a subsequence of @{text
   "\<alpha>\<^sub>1 \<Rightarrow> \<beta>\<^sub>1"}, @{text "\<beta>\<^sub>1 \<Rightarrow> \<alpha>\<^sub>1"}, \ldots, @{text "\<alpha>\<^sub>n \<Rightarrow> \<beta>\<^sub>n"}, @{text

--- a/src/Doc/Isar_Ref/Spec.thy	Mon Oct 12 21:15:10 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Oct 12 21:42:14 2015 +0200
@@ -1097,7 +1097,7 @@
   \[
     @{text "t :: (\<^vec>s\<^sub>1)c\<^sub>1 \<Longrightarrow> t :: (\<^vec>s\<^sub>2)c\<^sub>2 \<Longrightarrow> c\<^sub>1 \<subseteq> c\<^sub>2 \<Longrightarrow> \<^vec>s\<^sub>1 \<subseteq> \<^vec>s\<^sub>2"}
   \]
-  \noindent for all such arities.  In other words, whenever the result
+  for all such arities.  In other words, whenever the result
   classes of some type-constructor arities are related, then the
   argument sorts need to be related in the same way.