# HG changeset patch
# User wenzelm
# Date 1451141054 -3600
# Node ID 2e48182cc82c85312016955054e052aa201f56ad
# Parent  ed47044ee6a6478a4d6ac442eb74d48566f9ce4c
misc tuning and modernization;

diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Isar_Examples/Basic_Logic.thy
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
 Basic propositional and quantifier reasoning.
 *)
@@ -13,9 +13,11 @@
 
 subsection \<open>Pure backward reasoning\<close>
 
-text \<open>In order to get a first idea of how Isabelle/Isar proof documents may
-  look like, we consider the propositions \<open>I\<close>, \<open>K\<close>, and \<open>S\<close>. The following
-  (rather explicit) proofs should require little extra explanations.\<close>
+text \<open>
+  In order to get a first idea of how Isabelle/Isar proof documents may look
+  like, we consider the propositions \<open>I\<close>, \<open>K\<close>, and \<open>S\<close>. The following (rather
+  explicit) proofs should require little extra explanations.
+\<close>
 
 lemma I: "A \<longrightarrow> A"
 proof
@@ -50,54 +52,52 @@
   qed
 qed
 
-text \<open>Isar provides several ways to fine-tune the reasoning, avoiding
-  excessive detail. Several abbreviated language elements are available,
-  enabling the writer to express proofs in a more concise way, even without
-  referring to any automated proof tools yet.
-
-  First of all, proof by assumption may be abbreviated as a single dot.\<close>
+text \<open>
+  Isar provides several ways to fine-tune the reasoning, avoiding excessive
+  detail. Several abbreviated language elements are available, enabling the
+  writer to express proofs in a more concise way, even without referring to
+  any automated proof tools yet.
 
-lemma "A \<longrightarrow> A"
-proof
-  assume A
-  show A by fact+
-qed
-
-text \<open>In fact, concluding any (sub-)proof already involves solving any
-  remaining goals by assumption\footnote{This is not a completely trivial
-  operation, as proof by assumption may involve full higher-order
-  unification.}. Thus we may skip the rather vacuous body of the above proof
-  as well.\<close>
+  Concluding any (sub-)proof already involves solving any remaining goals by
+  assumption\<^footnote>\<open>This is not a completely trivial operation, as proof by
+  assumption may involve full higher-order unification.\<close>. Thus we may skip the
+  rather vacuous body of the above proof.
+\<close>
 
 lemma "A \<longrightarrow> A"
 proof
 qed
 
-text \<open>Note that the \isacommand{proof} command refers to the \<open>rule\<close> method
-  (without arguments) by default. Thus it implicitly applies a single rule,
-  as determined from the syntactic form of the statements involved. The
-  \isacommand{by} command abbreviates any proof with empty body, so the
-  proof may be further pruned.\<close>
+text \<open>
+  Note that the \<^theory_text>\<open>proof\<close> command refers to the \<open>rule\<close> method (without
+  arguments) by default. Thus it implicitly applies a single rule, as
+  determined from the syntactic form of the statements involved. The \<^theory_text>\<open>by\<close>
+  command abbreviates any proof with empty body, so the proof may be further
+  pruned.
+\<close>
 
 lemma "A \<longrightarrow> A"
   by rule
 
-text \<open>Proof by a single rule may be abbreviated as double-dot.\<close>
+text \<open>
+  Proof by a single rule may be abbreviated as double-dot.
+\<close>
 
 lemma "A \<longrightarrow> A" ..
 
-text \<open>Thus we have arrived at an adequate representation of the proof of a
-  tautology that holds by a single standard rule.\footnote{Apparently, the
-  rule here is implication introduction.}
+text \<open>
+  Thus we have arrived at an adequate representation of the proof of a
+  tautology that holds by a single standard rule.\<^footnote>\<open>Apparently, the
+  rule here is implication introduction.\<close>
 
   \<^medskip>
   Let us also reconsider \<open>K\<close>. Its statement is composed of iterated
-  connectives. Basic decomposition is by a single rule at a time, which is
-  why our first version above was by nesting two proofs.
+  connectives. Basic decomposition is by a single rule at a time, which is why
+  our first version above was by nesting two proofs.
 
-  The \<open>intro\<close> proof method repeatedly decomposes a goal's
-  conclusion.\footnote{The dual method is \<open>elim\<close>, acting on a goal's
-  premises.}\<close>
+  The \<open>intro\<close> proof method repeatedly decomposes a goal's conclusion.\<^footnote>\<open>The
+  dual method is \<open>elim\<close>, acting on a goal's premises.\<close>
+\<close>
 
 lemma "A \<longrightarrow> B \<longrightarrow> A"
 proof (intro impI)
@@ -110,29 +110,32 @@
 lemma "A \<longrightarrow> B \<longrightarrow> A"
   by (intro impI)
 
-text \<open>Just like \<open>rule\<close>, the \<open>intro\<close> and \<open>elim\<close> proof methods pick standard
+text \<open>
+  Just like \<open>rule\<close>, the \<open>intro\<close> and \<open>elim\<close> proof methods pick standard
   structural rules, in case no explicit arguments are given. While implicit
-  rules are usually just fine for single rule application, this may go too
-  far with iteration. Thus in practice, \<open>intro\<close> and \<open>elim\<close> would be
-  typically restricted to certain structures by giving a few rules only,
-  e.g.\ \isacommand{proof}~\<open>(intro impI allI)\<close> to strip implications and
-  universal quantifiers.
+  rules are usually just fine for single rule application, this may go too far
+  with iteration. Thus in practice, \<open>intro\<close> and \<open>elim\<close> would be typically
+  restricted to certain structures by giving a few rules only, e.g.\ \<^theory_text>\<open>proof
+  (intro impI allI)\<close> to strip implications and universal quantifiers.
 
   Such well-tuned iterated decomposition of certain structures is the prime
-  application of \<open>intro\<close> and \<open>elim\<close>. In contrast, terminal steps that solve
-  a goal completely are usually performed by actual automated proof methods
-  (such as \isacommand{by}~\<open>blast\<close>.\<close>
+  application of \<open>intro\<close> and \<open>elim\<close>. In contrast, terminal steps that solve a
+  goal completely are usually performed by actual automated proof methods
+  (such as \<^theory_text>\<open>by blast\<close>.
+\<close>
 
 
 subsection \<open>Variations of backward vs.\ forward reasoning\<close>
 
-text \<open>Certainly, any proof may be performed in backward-style only. On the
-  other hand, small steps of reasoning are often more naturally expressed in
+text \<open>
+  Certainly, any proof may be performed in backward-style only. On the other
+  hand, small steps of reasoning are often more naturally expressed in
   forward-style. Isar supports both backward and forward reasoning as a
   first-class concept. In order to demonstrate the difference, we consider
   several proofs of \<open>A \<and> B \<longrightarrow> B \<and> A\<close>.
 
-  The first version is purely backward.\<close>
+  The first version is purely backward.
+\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -144,12 +147,13 @@
   qed
 qed
 
-text \<open>Above, the projection rules \<open>conjunct1\<close> / \<open>conjunct2\<close> had to be named
-  explicitly, since the goals \<open>B\<close> and \<open>A\<close> did not provide any structural
-  clue. This may be avoided using \isacommand{from} to focus on the \<open>A \<and> B\<close>
-  assumption as the current facts, enabling the use of double-dot proofs.
-  Note that \isacommand{from} already does forward-chaining, involving the
-  \<open>conjE\<close> rule here.\<close>
+text \<open>
+  Above, the projection rules \<open>conjunct1\<close> / \<open>conjunct2\<close> had to be named
+  explicitly, since the goals \<open>B\<close> and \<open>A\<close> did not provide any structural clue.
+  This may be avoided using \<^theory_text>\<open>from\<close> to focus on the \<open>A \<and> B\<close> assumption as the
+  current facts, enabling the use of double-dot proofs. Note that \<^theory_text>\<open>from\<close>
+  already does forward-chaining, involving the \<open>conjE\<close> rule here.
+\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -161,12 +165,14 @@
   qed
 qed
 
-text \<open>In the next version, we move the forward step one level upwards.
-  Forward-chaining from the most recent facts is indicated by the
-  \isacommand{then} command. Thus the proof of \<open>B \<and> A\<close> from \<open>A \<and> B\<close> actually
-  becomes an elimination, rather than an introduction. The resulting proof
-  structure directly corresponds to that of the \<open>conjE\<close> rule, including the
-  repeated goal proposition that is abbreviated as \<open>?thesis\<close> below.\<close>
+text \<open>
+  In the next version, we move the forward step one level upwards.
+  Forward-chaining from the most recent facts is indicated by the \<^theory_text>\<open>then\<close>
+  command. Thus the proof of \<open>B \<and> A\<close> from \<open>A \<and> B\<close> actually becomes an
+  elimination, rather than an introduction. The resulting proof structure
+  directly corresponds to that of the \<open>conjE\<close> rule, including the repeated
+  goal proposition that is abbreviated as \<open>?thesis\<close> below.
+\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -178,9 +184,11 @@
   qed
 qed
 
-text \<open>In the subsequent version we flatten the structure of the main body by
-  doing forward reasoning all the time. Only the outermost decomposition
-  step is left as backward.\<close>
+text \<open>
+  In the subsequent version we flatten the structure of the main body by doing
+  forward reasoning all the time. Only the outermost decomposition step is
+  left as backward.
+\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -190,9 +198,11 @@
   from \<open>B\<close> \<open>A\<close> show "B \<and> A" ..
 qed
 
-text \<open>We can still push forward-reasoning a bit further, even at the risk of
-  getting ridiculous. Note that we force the initial proof step to do
-  nothing here, by referring to the \<open>-\<close> proof method.\<close>
+text \<open>
+  We can still push forward-reasoning a bit further, even at the risk of
+  getting ridiculous. Note that we force the initial proof step to do nothing
+  here, by referring to the \<open>-\<close> proof method.
+\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof -
@@ -208,22 +218,22 @@
 text \<open>
   \<^medskip>
   With these examples we have shifted through a whole range from purely
-  backward to purely forward reasoning. Apparently, in the extreme ends we
-  get slightly ill-structured proofs, which also require much explicit
-  naming of either rules (backward) or local facts (forward).
+  backward to purely forward reasoning. Apparently, in the extreme ends we get
+  slightly ill-structured proofs, which also require much explicit naming of
+  either rules (backward) or local facts (forward).
 
-  The general lesson learned here is that good proof style would achieve
-  just the \<^emph>\<open>right\<close> balance of top-down backward decomposition, and
-  bottom-up forward composition. In general, there is no single best way to
-  arrange some pieces of formal reasoning, of course. Depending on the
-  actual applications, the intended audience etc., rules (and methods) on
-  the one hand vs.\ facts on the other hand have to be emphasized in an
-  appropriate way. This requires the proof writer to develop good taste, and
-  some practice, of course.
+  The general lesson learned here is that good proof style would achieve just
+  the \<^emph>\<open>right\<close> balance of top-down backward decomposition, and bottom-up
+  forward composition. In general, there is no single best way to arrange some
+  pieces of formal reasoning, of course. Depending on the actual applications,
+  the intended audience etc., rules (and methods) on the one hand vs.\ facts
+  on the other hand have to be emphasized in an appropriate way. This requires
+  the proof writer to develop good taste, and some practice, of course.
 
   \<^medskip>
-  For our example the most appropriate way of reasoning is probably the
-  middle one, with conjunction introduction done after elimination.\<close>
+  For our example the most appropriate way of reasoning is probably the middle
+  one, with conjunction introduction done after elimination.
+\<close>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -239,15 +249,19 @@
 
 subsection \<open>A few examples from ``Introduction to Isabelle''\<close>
 
-text \<open>We rephrase some of the basic reasoning examples of @{cite
-  "isabelle-intro"}, using HOL rather than FOL.\<close>
+text \<open>
+  We rephrase some of the basic reasoning examples of @{cite
+  "isabelle-intro"}, using HOL rather than FOL.
+\<close>
 
 
 subsubsection \<open>A propositional proof\<close>
 
-text \<open>We consider the proposition \<open>P \<or> P \<longrightarrow> P\<close>. The proof below involves
-  forward-chaining from \<open>P \<or> P\<close>, followed by an explicit case-analysis on
-  the two \<^emph>\<open>identical\<close> cases.\<close>
+text \<open>
+  We consider the proposition \<open>P \<or> P \<longrightarrow> P\<close>. The proof below involves
+  forward-chaining from \<open>P \<or> P\<close>, followed by an explicit case-analysis on the
+  two \<^emph>\<open>identical\<close> cases.
+\<close>
 
 lemma "P \<or> P \<longrightarrow> P"
 proof
@@ -260,9 +274,10 @@
   qed
 qed
 
-text \<open>Case splits are \<^emph>\<open>not\<close> hardwired into the Isar language as a
-  special feature. The \isacommand{next} command used to separate the cases
-  above is just a short form of managing block structure.
+text \<open>
+  Case splits are \<^emph>\<open>not\<close> hardwired into the Isar language as a special
+  feature. The \<^theory_text>\<open>next\<close> command used to separate the cases above is just a
+  short form of managing block structure.
 
   \<^medskip>
   In general, applying proof methods may split up a goal into separate
@@ -270,17 +285,17 @@
   corresponding proof text typically mimics this by establishing results in
   appropriate contexts, separated by blocks.
 
-  In order to avoid too much explicit parentheses, the Isar system
-  implicitly opens an additional block for any new goal, the
-  \isacommand{next} statement then closes one block level, opening a new
-  one. The resulting behaviour is what one would expect from separating
-  cases, only that it is more flexible. E.g.\ an induction base case (which
-  does not introduce local assumptions) would \<^emph>\<open>not\<close> require
-  \isacommand{next} to separate the subsequent step case.
+  In order to avoid too much explicit parentheses, the Isar system implicitly
+  opens an additional block for any new goal, the \<^theory_text>\<open>next\<close> statement then
+  closes one block level, opening a new one. The resulting behaviour is what
+  one would expect from separating cases, only that it is more flexible. E.g.\
+  an induction base case (which does not introduce local assumptions) would
+  \<^emph>\<open>not\<close> require \<^theory_text>\<open>next\<close> to separate the subsequent step case.
 
   \<^medskip>
   In our example the situation is even simpler, since the two cases actually
-  coincide. Consequently the proof may be rephrased as follows.\<close>
+  coincide. Consequently the proof may be rephrased as follows.
+\<close>
 
 lemma "P \<or> P \<longrightarrow> P"
 proof
@@ -307,16 +322,17 @@
 
 subsubsection \<open>A quantifier proof\<close>
 
-text \<open>To illustrate quantifier reasoning, let us prove
+text \<open>
+  To illustrate quantifier reasoning, let us prove
   \<open>(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)\<close>. Informally, this holds because any \<open>a\<close> with
   \<open>P (f a)\<close> may be taken as a witness for the second existential statement.
 
   The first proof is rather verbose, exhibiting quite a lot of (redundant)
-  detail. It gives explicit rules, even with some instantiation.
-  Furthermore, we encounter two new language elements: the \isacommand{fix}
-  command augments the context by some new ``arbitrary, but fixed'' element;
-  the \isacommand{is} annotation binds term abbreviations by higher-order
-  pattern matching.\<close>
+  detail. It gives explicit rules, even with some instantiation. Furthermore,
+  we encounter two new language elements: the \<^theory_text>\<open>fix\<close> command augments the
+  context by some new ``arbitrary, but fixed'' element; the \<^theory_text>\<open>is\<close> annotation
+  binds term abbreviations by higher-order pattern matching.
+\<close>
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
@@ -329,11 +345,13 @@
   qed
 qed
 
-text \<open>While explicit rule instantiation may occasionally improve readability
-  of certain aspects of reasoning, it is usually quite redundant. Above, the
-  basic proof outline gives already enough structural clues for the system
-  to infer both the rules and their instances (by higher-order unification).
-  Thus we may as well prune the text as follows.\<close>
+text \<open>
+  While explicit rule instantiation may occasionally improve readability of
+  certain aspects of reasoning, it is usually quite redundant. Above, the
+  basic proof outline gives already enough structural clues for the system to
+  infer both the rules and their instances (by higher-order unification). Thus
+  we may as well prune the text as follows.
+\<close>
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
@@ -346,9 +364,11 @@
   qed
 qed
 
-text \<open>Explicit \<open>\<exists>\<close>-elimination as seen above can become quite cumbersome in
-  practice. The derived Isar language element ``\isakeyword{obtain}''
-  provides a more handsome way to do generalized existence reasoning.\<close>
+text \<open>
+  Explicit \<open>\<exists>\<close>-elimination as seen above can become quite cumbersome in
+  practice. The derived Isar language element ``\<^theory_text>\<open>obtain\<close>'' provides a more
+  handsome way to do generalized existence reasoning.
+\<close>
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
@@ -357,19 +377,22 @@
   then show "\<exists>y. P y" ..
 qed
 
-text \<open>Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
-  \isakeyword{assume} together with a soundness proof of the elimination
-  involved. Thus it behaves similar to any other forward proof element. Also
-  note that due to the nature of general existence reasoning involved here,
-  any result exported from the context of an \isakeyword{obtain} statement
-  may \<^emph>\<open>not\<close> refer to the parameters introduced there.\<close>
+text \<open>
+  Technically, \<^theory_text>\<open>obtain\<close> is similar to \<^theory_text>\<open>fix\<close> and \<^theory_text>\<open>assume\<close> together with a
+  soundness proof of the elimination involved. Thus it behaves similar to any
+  other forward proof element. Also note that due to the nature of general
+  existence reasoning involved here, any result exported from the context of
+  an \<^theory_text>\<open>obtain\<close> statement may \<^emph>\<open>not\<close> refer to the parameters introduced there.
+\<close>
 
 
 subsubsection \<open>Deriving rules in Isabelle\<close>
 
-text \<open>We derive the conjunction elimination rule from the corresponding
+text \<open>
+  We derive the conjunction elimination rule from the corresponding
   projections. The proof is quite straight-forward, since Isabelle/Isar
-  supports non-atomic goals and assumptions fully transparently.\<close>
+  supports non-atomic goals and assumptions fully transparently.
+\<close>
 
 theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
 proof -
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Drinker.thy
--- a/src/HOL/Isar_Examples/Drinker.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Drinker.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -8,11 +8,12 @@
 imports Main
 begin
 
-text \<open>Here is another example of classical reasoning: the Drinker's
-  Principle says that for some person, if he is drunk, everybody else is
-  drunk!
+text \<open>
+  Here is another example of classical reasoning: the Drinker's Principle says
+  that for some person, if he is drunk, everybody else is drunk!
 
-  We first prove a classical part of de-Morgan's law.\<close>
+  We first prove a classical part of de-Morgan's law.
+\<close>
 
 lemma de_Morgan:
   assumes "\<not> (\<forall>x. P x)"
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Expr_Compiler.thy
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Isar_Examples/Expr_Compiler.thy
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
 Correctness of a simple expression/stack-machine compiler.
 *)
@@ -10,32 +10,40 @@
 imports Main
 begin
 
-text \<open>This is a (rather trivial) example of program verification. We model a
+text \<open>
+  This is a (rather trivial) example of program verification. We model a
   compiler for translating expressions to stack machine instructions, and
-  prove its correctness wrt.\ some evaluation semantics.\<close>
+  prove its correctness wrt.\ some evaluation semantics.
+\<close>
 
 
 subsection \<open>Binary operations\<close>
 
-text \<open>Binary operations are just functions over some type of values. This is
-  both for abstract syntax and semantics, i.e.\ we use a ``shallow
-  embedding'' here.\<close>
+text \<open>
+  Binary operations are just functions over some type of values. This is both
+  for abstract syntax and semantics, i.e.\ we use a ``shallow embedding''
+  here.
+\<close>
 
 type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> 'val"
 
 
 subsection \<open>Expressions\<close>
 
-text \<open>The language of expressions is defined as an inductive type,
-  consisting of variables, constants, and binary operations on expressions.\<close>
+text \<open>
+  The language of expressions is defined as an inductive type, consisting of
+  variables, constants, and binary operations on expressions.
+\<close>
 
 datatype (dead 'adr, dead 'val) expr =
     Variable 'adr
   | Constant 'val
   | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
 
-text \<open>Evaluation (wrt.\ some environment of variable assignments) is defined
-  by primitive recursion over the structure of expressions.\<close>
+text \<open>
+  Evaluation (wrt.\ some environment of variable assignments) is defined by
+  primitive recursion over the structure of expressions.
+\<close>
 
 primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val"
 where
@@ -46,15 +54,19 @@
 
 subsection \<open>Machine\<close>
 
-text \<open>Next we model a simple stack machine, with three instructions.\<close>
+text \<open>
+  Next we model a simple stack machine, with three instructions.
+\<close>
 
 datatype (dead 'adr, dead 'val) instr =
     Const 'val
   | Load 'adr
   | Apply "'val binop"
 
-text \<open>Execution of a list of stack machine instructions is easily defined as
-  follows.\<close>
+text \<open>
+  Execution of a list of stack machine instructions is easily defined as
+  follows.
+\<close>
 
 primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> 'val list"
 where
@@ -72,8 +84,10 @@
 
 subsection \<open>Compiler\<close>
 
-text \<open>We are ready to define the compilation function of expressions to
-  lists of stack machine instructions.\<close>
+text \<open>
+  We are ready to define the compilation function of expressions to lists of
+  stack machine instructions.
+\<close>
 
 primrec compile :: "('adr, 'val) expr \<Rightarrow> (('adr, 'val) instr) list"
 where
@@ -82,8 +96,10 @@
 | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
 
 
-text \<open>The main result of this development is the correctness theorem for
-  \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.\<close>
+text \<open>
+  The main result of this development is the correctness theorem for
+  \<open>compile\<close>. We first establish a lemma about \<open>exec\<close> and list append.
+\<close>
 
 lemma exec_append:
   "exec (xs @ ys) stack env =
@@ -128,8 +144,8 @@
   In the proofs above, the \<open>simp\<close> method does quite a lot of work behind the
   scenes (mostly ``functional program execution''). Subsequently, the same
   reasoning is elaborated in detail --- at most one recursive function
-  definition is used at a time. Thus we get a better idea of what is
-  actually going on.
+  definition is used at a time. Thus we get a better idea of what is actually
+  going on.
 \<close>
 
 lemma exec_append':
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -18,9 +18,8 @@
 imports "../Number_Theory/Primes"
 begin
 
-text_raw \<open>\footnote{Isar version by Gertrud Bauer.  Original tactic
-  script by Larry Paulson.  A few proofs of laws taken from
-  @{cite "Concrete-Math"}.}\<close>
+text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
+  Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
 
 
 declare One_nat_def [simp]
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Group.thy
--- a/src/HOL/Isar_Examples/Group.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Group.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Isar_Examples/Group.thy
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 *)
 
 section \<open>Basic group theory\<close>
@@ -10,17 +10,21 @@
 
 subsection \<open>Groups and calculational reasoning\<close> 
 
-text \<open>Groups over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close>
-  are defined as an axiomatic type class as follows. Note that the parent
-  class \<open>times\<close> is provided by the basic HOL theory.\<close>
+text \<open>
+  Groups over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>, inverse :: \<alpha> \<Rightarrow> \<alpha>)\<close> are
+  defined as an axiomatic type class as follows. Note that the parent class
+  \<open>times\<close> is provided by the basic HOL theory.
+\<close>
 
 class group = times + one + inverse +
   assumes group_assoc: "(x * y) * z = x * (y * z)"
     and group_left_one: "1 * x = x"
     and group_left_inverse: "inverse x * x = 1"
 
-text \<open>The group axioms only state the properties of left one and inverse,
-  the right versions may be derived as follows.\<close>
+text \<open>
+  The group axioms only state the properties of left one and inverse, the
+  right versions may be derived as follows.
+\<close>
 
 theorem (in group) group_right_inverse: "x * inverse x = 1"
 proof -
@@ -43,8 +47,10 @@
   finally show ?thesis .
 qed
 
-text \<open>With \<open>group_right_inverse\<close> already available, \<open>group_right_one\<close>
-  \label{thm:group-right-one} is now established much easier.\<close>
+text \<open>
+  With \<open>group_right_inverse\<close> already available, \<open>group_right_one\<close>
+  is now established much easier.
+\<close>
 
 theorem (in group) group_right_one: "x * 1 = x"
 proof -
@@ -63,23 +69,23 @@
   \<^medskip>
   The calculational proof style above follows typical presentations given in
   any introductory course on algebra. The basic technique is to form a
-  transitive chain of equations, which in turn are established by
-  simplifying with appropriate rules. The low-level logical details of
-  equational reasoning are left implicit.
+  transitive chain of equations, which in turn are established by simplifying
+  with appropriate rules. The low-level logical details of equational
+  reasoning are left implicit.
 
   Note that ``\<open>\<dots>\<close>'' is just a special term variable that is bound
-  automatically to the argument\footnote{The argument of a curried infix
-  expression happens to be its right-hand side.} of the last fact achieved
-  by any local assumption or proven statement. In contrast to \<open>?thesis\<close>, the
-  ``\<open>\<dots>\<close>'' variable is bound \<^emph>\<open>after\<close> the proof is finished.
+  automatically to the argument\<^footnote>\<open>The argument of a curried infix expression
+  happens to be its right-hand side.\<close> of the last fact achieved by any local
+  assumption or proven statement. In contrast to \<open>?thesis\<close>, the ``\<open>\<dots>\<close>''
+  variable is bound \<^emph>\<open>after\<close> the proof is finished.
 
-  There are only two separate Isar language elements for calculational
-  proofs: ``\isakeyword{also}'' for initial or intermediate calculational
-  steps, and ``\isakeyword{finally}'' for exhibiting the result of a
-  calculation. These constructs are not hardwired into Isabelle/Isar, but
-  defined on top of the basic Isar/VM interpreter. Expanding the
-  \isakeyword{also} and \isakeyword{finally} derived language elements,
-  calculations may be simulated by hand as demonstrated below.\<close>
+  There are only two separate Isar language elements for calculational proofs:
+  ``\<^theory_text>\<open>also\<close>'' for initial or intermediate calculational steps, and
+  ``\<^theory_text>\<open>finally\<close>'' for exhibiting the result of a calculation. These constructs
+  are not hardwired into Isabelle/Isar, but defined on top of the basic
+  Isar/VM interpreter. Expanding the \<^theory_text>\<open>also\<close> and \<^theory_text>\<open>finally\<close> derived language
+  elements, calculations may be simulated by hand as demonstrated below.
+\<close>
 
 theorem (in group) "x * 1 = x"
 proof -
@@ -112,30 +118,35 @@
   show ?thesis .
 qed
 
-text \<open>Note that this scheme of calculations is not restricted to plain
+text \<open>
+  Note that this scheme of calculations is not restricted to plain
   transitivity. Rules like anti-symmetry, or even forward and backward
-  substitution work as well. For the actual implementation of
-  \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
-  separate context information of ``transitivity'' rules. Rule selection
-  takes place automatically by higher-order unification.\<close>
+  substitution work as well. For the actual implementation of \<^theory_text>\<open>also\<close> and
+  \<^theory_text>\<open>finally\<close>, Isabelle/Isar maintains separate context information of
+  ``transitivity'' rules. Rule selection takes place automatically by
+  higher-order unification.
+\<close>
 
 
 subsection \<open>Groups as monoids\<close>
 
-text \<open>Monoids over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>)\<close> are defined like
-  this.\<close>
+text \<open>
+  Monoids over signature \<open>(* :: \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>, 1 :: \<alpha>)\<close> are defined like this.
+\<close>
 
 class monoid = times + one +
   assumes monoid_assoc: "(x * y) * z = x * (y * z)"
     and monoid_left_one: "1 * x = x"
     and monoid_right_one: "x * 1 = x"
 
-text \<open>Groups are \<^emph>\<open>not\<close> yet monoids directly from the definition. For
-  monoids, \<open>right_one\<close> had to be included as an axiom, but for groups both
-  \<open>right_one\<close> and \<open>right_inverse\<close> are derivable from the other axioms. With
-  \<open>group_right_one\<close> derived as a theorem of group theory (see
-  page~\pageref{thm:group-right-one}), we may still instantiate
-  \<open>group \<subseteq> monoid\<close> properly as follows.\<close>
+text \<open>
+  Groups are \<^emph>\<open>not\<close> yet monoids directly from the definition. For monoids,
+  \<open>right_one\<close> had to be included as an axiom, but for groups both \<open>right_one\<close>
+  and \<open>right_inverse\<close> are derivable from the other axioms. With
+  \<open>group_right_one\<close> derived as a theorem of group theory (see @{thm
+  group_right_one}), we may still instantiate \<open>group \<subseteq> monoid\<close> properly as
+  follows.
+\<close>
 
 instance group \<subseteq> monoid
   by intro_classes
@@ -143,18 +154,21 @@
       rule group_left_one,
       rule group_right_one)
 
-text \<open>The \isacommand{instance} command actually is a version of
-  \isacommand{theorem}, setting up a goal that reflects the intended class
-  relation (or type constructor arity). Thus any Isar proof language element
-  may be involved to establish this statement. When concluding the proof,
-  the result is transformed into the intended type signature extension
-  behind the scenes.\<close>
+text \<open>
+  The \<^theory_text>\<open>instance\<close> command actually is a version of \<^theory_text>\<open>theorem\<close>, setting up a
+  goal that reflects the intended class relation (or type constructor arity).
+  Thus any Isar proof language element may be involved to establish this
+  statement. When concluding the proof, the result is transformed into the
+  intended type signature extension behind the scenes.
+\<close>
 
 
 subsection \<open>More theorems of group theory\<close>
 
-text \<open>The one element is already uniquely determined by preserving
-  an \<^emph>\<open>arbitrary\<close> group element.\<close>
+text \<open>
+  The one element is already uniquely determined by preserving an \<^emph>\<open>arbitrary\<close>
+  group element.
+\<close>
 
 theorem (in group) group_one_equality:
   assumes eq: "e * x = x"
@@ -173,7 +187,9 @@
   finally show ?thesis .
 qed
 
-text \<open>Likewise, the inverse is already determined by the cancel property.\<close>
+text \<open>
+  Likewise, the inverse is already determined by the cancel property.
+\<close>
 
 theorem (in group) group_inverse_equality:
   assumes eq: "x' * x = 1"
@@ -192,7 +208,9 @@
   finally show ?thesis .
 qed
 
-text \<open>The inverse operation has some further characteristic properties.\<close>
+text \<open>
+  The inverse operation has some further characteristic properties.
+\<close>
 
 theorem (in group) group_inverse_times: "inverse (x * y) = inverse y * inverse x"
 proof (rule group_inverse_equality)
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Isar_Examples/Hoare.thy
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
 A formulation of Hoare logic suitable for Isar.
 *)
@@ -12,10 +12,12 @@
 
 subsection \<open>Abstract syntax and semantics\<close>
 
-text \<open>The following abstract syntax and semantics of Hoare Logic over
-  \<^verbatim>\<open>WHILE\<close> programs closely follows the existing tradition in Isabelle/HOL
-  of formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See
-  also @{file "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.\<close>
+text \<open>
+  The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
+  programs closely follows the existing tradition in Isabelle/HOL of
+  formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
+  @{file "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.
+\<close>
 
 type_synonym 'a bexp = "'a set"
 type_synonym 'a assn = "'a set"
@@ -59,15 +61,17 @@
 
 subsection \<open>Primitive Hoare rules\<close>
 
-text \<open>From the semantics defined above, we derive the standard set of
-  primitive Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually,
-  variant forms of these rules are applied in actual proof, see also
-  \S\ref{sec:hoare-isar} and \S\ref{sec:hoare-vcg}.
+text \<open>
+  From the semantics defined above, we derive the standard set of primitive
+  Hoare rules; e.g.\ see @{cite \<open>\S6\<close> "Winskel:1993"}. Usually, variant forms
+  of these rules are applied in actual proof, see also \S\ref{sec:hoare-isar}
+  and \S\ref{sec:hoare-vcg}.
 
   \<^medskip>
   The \<open>basic\<close> rule represents any kind of atomic access to the state space.
   This subsumes the common rules of \<open>skip\<close> and \<open>assign\<close>, as formulated in
-  \S\ref{sec:hoare-isar}.\<close>
+  \S\ref{sec:hoare-isar}.
+\<close>
 
 theorem basic: "\<turnstile> {s. f s \<in> P} (Basic f) P"
 proof
@@ -78,8 +82,10 @@
   with s show "s' \<in> P" by simp
 qed
 
-text \<open>The rules for sequential commands and semantic consequences are
-  established in a straight forward manner as follows.\<close>
+text \<open>
+  The rules for sequential commands and semantic consequences are established
+  in a straight forward manner as follows.
+\<close>
 
 theorem seq: "\<turnstile> P c1 Q \<Longrightarrow> \<turnstile> Q c2 R \<Longrightarrow> \<turnstile> P (c1; c2) R"
 proof
@@ -104,9 +110,10 @@
   with QQ' show "s' \<in> Q'" ..
 qed
 
-text \<open>The rule for conditional commands is directly reflected by the
-  corresponding semantics; in the proof we just have to look closely which
-  cases apply.\<close>
+text \<open>
+  The rule for conditional commands is directly reflected by the corresponding
+  semantics; in the proof we just have to look closely which cases apply.
+\<close>
 
 theorem cond:
   assumes case_b: "\<turnstile> (P \<inter> b) c1 Q"
@@ -134,11 +141,13 @@
   qed
 qed
 
-text \<open>The \<open>while\<close> rule is slightly less trivial --- it is the only one based
-  on recursion, which is expressed in the semantics by a Kleene-style least
+text \<open>
+  The \<open>while\<close> rule is slightly less trivial --- it is the only one based on
+  recursion, which is expressed in the semantics by a Kleene-style least
   fixed-point construction. The auxiliary statement below, which is by
   induction on the number of iterations is the main point to be proven; the
-  rest is by routine application of the semantics of \<^verbatim>\<open>WHILE\<close>.\<close>
+  rest is by routine application of the semantics of \<^verbatim>\<open>WHILE\<close>.
+\<close>
 
 theorem while:
   assumes body: "\<turnstile> (P \<inter> b) c P"
@@ -164,13 +173,14 @@
 
 subsection \<open>Concrete syntax for assertions\<close>
 
-text \<open>We now introduce concrete syntax for describing commands (with
-  embedded expressions) and assertions. The basic technique is that of
-  semantic ``quote-antiquote''. A \<^emph>\<open>quotation\<close> is a syntactic entity
-  delimited by an implicit abstraction, say over the state space. An
-  \<^emph>\<open>antiquotation\<close> is a marked expression within a quotation that refers the
-  implicit argument; a typical antiquotation would select (or even update)
-  components from the state.
+text \<open>
+  We now introduce concrete syntax for describing commands (with embedded
+  expressions) and assertions. The basic technique is that of semantic
+  ``quote-antiquote''. A \<^emph>\<open>quotation\<close> is a syntactic entity delimited by an
+  implicit abstraction, say over the state space. An \<^emph>\<open>antiquotation\<close> is a
+  marked expression within a quotation that refers the implicit argument; a
+  typical antiquotation would select (or even update) components from the
+  state.
 
   We will see some examples later in the concrete rules and applications.
 
@@ -182,7 +192,8 @@
   concrete syntactic representation of our Hoare language, the actual ``ML
   drivers'' is quite involved. Just note that the we re-use the basic
   quote/antiquote translations as already defined in Isabelle/Pure (see @{ML
-  Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},).\<close>
+  Syntax_Trans.quote_tr}, and @{ML Syntax_Trans.quote_tr'},).
+\<close>
 
 syntax
   "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"
@@ -211,9 +222,11 @@
   in [(@{syntax_const "_quote"}, K quote_tr)] end
 \<close>
 
-text \<open>As usual in Isabelle syntax translations, the part for printing is
-  more complicated --- we cannot express parts as macro rules as above.
-  Don't look here, unless you have to do similar things for yourself.\<close>
+text \<open>
+  As usual in Isabelle syntax translations, the part for printing is more
+  complicated --- we cannot express parts as macro rules as above. Don't look
+  here, unless you have to do similar things for yourself.
+\<close>
 
 print_translation \<open>
   let
@@ -242,14 +255,16 @@
 
 subsection \<open>Rules for single-step proof \label{sec:hoare-isar}\<close>
 
-text \<open>We are now ready to introduce a set of Hoare rules to be used in
-  single-step structured proofs in Isabelle/Isar. We refer to the concrete
-  syntax introduce above.
+text \<open>
+  We are now ready to introduce a set of Hoare rules to be used in single-step
+  structured proofs in Isabelle/Isar. We refer to the concrete syntax
+  introduce above.
 
   \<^medskip>
   Assertions of Hoare Logic may be manipulated in calculational proofs, with
   the inclusion expressed in terms of sets or predicates. Reversed order is
-  supported as well.\<close>
+  supported as well.
+\<close>
 
 lemma [trans]: "\<turnstile> P c Q \<Longrightarrow> P' \<subseteq> P \<Longrightarrow> \<turnstile> P' c Q"
   by (unfold Valid_def) blast
@@ -276,10 +291,11 @@
   by (simp add: Valid_def)
 
 
-text \<open>Identity and basic assignments.\footnote{The \<open>hoare\<close> method introduced
-  in \S\ref{sec:hoare-vcg} is able to provide proper instances for any
-  number of basic assignments, without producing additional verification
-  conditions.}\<close>
+text \<open>
+  Identity and basic assignments.\<^footnote>\<open>The \<open>hoare\<close> method introduced in
+  \S\ref{sec:hoare-vcg} is able to provide proper instances for any number of
+  basic assignments, without producing additional verification conditions.\<close>
+\<close>
 
 lemma skip [intro?]: "\<turnstile> P SKIP P"
 proof -
@@ -290,20 +306,22 @@
 lemma assign: "\<turnstile> P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   by (rule basic)
 
-text \<open>Note that above formulation of assignment corresponds to our
-  preferred way to model state spaces, using (extensible) record types in
-  HOL @{cite "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>,
-  Isabelle/HOL provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update).
-  Above, there is only a place-holder appearing for the latter kind of
-  function: due to concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains
-  \<open>x_update\<close>.\footnote{Note that due to the external nature of HOL record
-  fields, we could not even state a general theorem relating selector and
-  update functions (if this were required here); this would only work for
-  any particular instance of record fields introduced so far.}
+text \<open>
+  Note that above formulation of assignment corresponds to our preferred way
+  to model state spaces, using (extensible) record types in HOL @{cite
+  "Naraschewski-Wenzel:1998:HOOL"}. For any record field \<open>x\<close>, Isabelle/HOL
+  provides a functions \<open>x\<close> (selector) and \<open>x_update\<close> (update). Above, there is
+  only a place-holder appearing for the latter kind of function: due to
+  concrete syntax \<open>\<acute>x := \<acute>a\<close> also contains \<open>x_update\<close>.\<^footnote>\<open>Note that due to the
+  external nature of HOL record fields, we could not even state a general
+  theorem relating selector and update functions (if this were required here);
+  this would only work for any particular instance of record fields introduced
+  so far.\<close>
 
   \<^medskip>
-  Sequential composition --- normalizing with associativity achieves proper
-  of chunks of code verified separately.\<close>
+  Sequential composition --- normalizing with associativity achieves proper of
+  chunks of code verified separately.
+\<close>
 
 lemmas [trans, intro?] = seq
 
@@ -342,15 +360,17 @@
 
 subsection \<open>Verification conditions \label{sec:hoare-vcg}\<close>
 
-text \<open>We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic
-  definition for the Hoare Verification Condition Generator (see @{file
+text \<open>
+  We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition
+  for the Hoare Verification Condition Generator (see @{file
   "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a
   proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to
-  extract purely logical verification conditions. It is important to note
-  that the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with
-  invariants beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are
-  handled --- the underlying tactic fails ungracefully if supplied with
-  meta-variables or parameters, for example.\<close>
+  extract purely logical verification conditions. It is important to note that
+  the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants
+  beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the
+  underlying tactic fails ungracefully if supplied with meta-variables or
+  parameters, for example.
+\<close>
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
   by (auto simp add: Valid_def)
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -6,9 +6,11 @@
 
 subsection \<open>State spaces\<close>
 
-text \<open>First of all we provide a store of program variables that occur in any
-  of the programs considered later. Slightly unexpected things may happen
-  when attempting to work with undeclared variables.\<close>
+text \<open>
+  First of all we provide a store of program variables that occur in any of
+  the programs considered later. Slightly unexpected things may happen when
+  attempting to work with undeclared variables.
+\<close>
 
 record vars =
   I :: nat
@@ -16,28 +18,33 @@
   N :: nat
   S :: nat
 
-text \<open>While all of our variables happen to have the same type, nothing would
+text \<open>
+  While all of our variables happen to have the same type, nothing would
   prevent us from working with many-sorted programs as well, or even
-  polymorphic ones. Also note that Isabelle/HOL's extensible record types
-  even provides simple means to extend the state space later.\<close>
+  polymorphic ones. Also note that Isabelle/HOL's extensible record types even
+  provides simple means to extend the state space later.
+\<close>
 
 
 subsection \<open>Basic examples\<close>
 
-text \<open>We look at few trivialities involving assignment and sequential
-  composition, in order to get an idea of how to work with our formulation
-  of Hoare Logic.\<close>
+text \<open>
+  We look at few trivialities involving assignment and sequential composition,
+  in order to get an idea of how to work with our formulation of Hoare Logic.
 
-text \<open>Using the basic \<open>assign\<close> rule directly is a bit
-  cumbersome.\<close>
+  \<^medskip>
+  Using the basic \<open>assign\<close> rule directly is a bit cumbersome.
+\<close>
 
 lemma "\<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
   by (rule assign)
 
-text \<open>Certainly we want the state modification already done, e.g.\ by
+text \<open>
+  Certainly we want the state modification already done, e.g.\ by
   simplification. The \<open>hoare\<close> method performs the basic state update for us;
   we may apply the Simplifier afterwards to achieve ``obvious'' consequences
-  as well.\<close>
+  as well.
+\<close>
 
 lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>"
   by hoare
@@ -66,10 +73,12 @@
       \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
   by hoare simp
 
-text \<open>It is important to note that statements like the following one can
-  only be proven for each individual program variable. Due to the
-  extra-logical nature of record fields, we cannot formulate a theorem
-  relating record selectors and updates schematically.\<close>
+text \<open>
+  It is important to note that statements like the following one can only be
+  proven for each individual program variable. Due to the extra-logical nature
+  of record fields, we cannot formulate a theorem relating record selectors
+  and updates schematically.
+\<close>
 
 lemma "\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N := \<acute>N \<lbrace>\<acute>N = a\<rbrace>"
   by hoare
@@ -83,9 +92,11 @@
   oops
 
 
-text \<open>In the following assignments we make use of the consequence rule in
-  order to achieve the intended precondition. Certainly, the \<open>hoare\<close> method
-  is able to handle this case, too.\<close>
+text \<open>
+  In the following assignments we make use of the consequence rule in order to
+  achieve the intended precondition. Certainly, the \<open>hoare\<close> method is able to
+  handle this case, too.
+\<close>
 
 lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
 proof -
@@ -113,10 +124,12 @@
 
 subsection \<open>Multiplication by addition\<close>
 
-text \<open>We now do some basic examples of actual \<^verbatim>\<open>WHILE\<close> programs. This one is
-  a loop for calculating the product of two natural numbers, by iterated
-  addition. We first give detailed structured proof based on single-step
-  Hoare rules.\<close>
+text \<open>
+  We now do some basic examples of actual \<^verbatim>\<open>WHILE\<close> programs. This one is a
+  loop for calculating the product of two natural numbers, by iterated
+  addition. We first give detailed structured proof based on single-step Hoare
+  rules.
+\<close>
 
 lemma
   "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@@ -140,10 +153,12 @@
   finally show ?thesis .
 qed
 
-text \<open>The subsequent version of the proof applies the \<open>hoare\<close> method to
-  reduce the Hoare statement to a purely logical problem that can be solved
-  fully automatically. Note that we have to specify the \<^verbatim>\<open>WHILE\<close> loop
-  invariant in the original statement.\<close>
+text \<open>
+  The subsequent version of the proof applies the \<open>hoare\<close> method to reduce the
+  Hoare statement to a purely logical problem that can be solved fully
+  automatically. Note that we have to specify the \<^verbatim>\<open>WHILE\<close> loop invariant in
+  the original statement.
+\<close>
 
 lemma
   "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
@@ -156,15 +171,16 @@
 
 subsection \<open>Summing natural numbers\<close>
 
-text \<open>We verify an imperative program to sum natural numbers up to a given
-  limit. First some functional definition for proper specification of the
-  problem.
+text \<open>
+  We verify an imperative program to sum natural numbers up to a given limit.
+  First some functional definition for proper specification of the problem.
 
   \<^medskip>
   The following proof is quite explicit in the individual steps taken, with
   the \<open>hoare\<close> method only applied locally to take care of assignment and
   sequential composition. Note that we express intermediate proof obligation
-  in pure logic, without referring to the state space.\<close>
+  in pure logic, without referring to the state space.
+\<close>
 
 theorem
   "\<turnstile> \<lbrace>True\<rbrace>
@@ -202,8 +218,10 @@
   finally show ?thesis .
 qed
 
-text \<open>The next version uses the \<open>hoare\<close> method, while still explaining the
-  resulting proof obligations in an abstract, structured manner.\<close>
+text \<open>
+  The next version uses the \<open>hoare\<close> method, while still explaining the
+  resulting proof obligations in an abstract, structured manner.
+\<close>
 
 theorem
   "\<turnstile> \<lbrace>True\<rbrace>
@@ -228,8 +246,10 @@
   qed
 qed
 
-text \<open>Certainly, this proof may be done fully automatic as well, provided
-  that the invariant is given beforehand.\<close>
+text \<open>
+  Certainly, this proof may be done fully automatic as well, provided that the
+  invariant is given beforehand.
+\<close>
 
 theorem
   "\<turnstile> \<lbrace>True\<rbrace>
@@ -246,8 +266,10 @@
 
 subsection \<open>Time\<close>
 
-text \<open>A simple embedding of time in Hoare logic: function \<open>timeit\<close> inserts
-  an extra variable to keep track of the elapsed time.\<close>
+text \<open>
+  A simple embedding of time in Hoare logic: function \<open>timeit\<close> inserts an
+  extra variable to keep track of the elapsed time.
+\<close>
 
 record tstate = time :: nat
 
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Knaster_Tarski.thy
--- a/src/HOL/Isar_Examples/Knaster_Tarski.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Knaster_Tarski.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Isar_Examples/Knaster_Tarski.thy
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 
 Typical textbook proof example.
 *)
@@ -13,28 +13,30 @@
 
 subsection \<open>Prose version\<close>
 
-text \<open>According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"},
-  the Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
-  dualized the argument, and tuned the notation a little bit.}
+text \<open>
+  According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"}, the
+  Knaster-Tarski fixpoint theorem is as follows.\<^footnote>\<open>We have dualized the
+  argument, and tuned the notation a little bit.\<close>
 
   \<^bold>\<open>The Knaster-Tarski Fixpoint Theorem.\<close> Let \<open>L\<close> be a complete lattice and
-  \<open>f: L \<rightarrow> L\<close> an order-preserving map. Then \<open>\<Sqinter>{x \<in> L | f(x) \<le> x}\<close> is a
-  fixpoint of \<open>f\<close>.
+  \<open>f: L \<rightarrow> L\<close> an order-preserving map. Then \<open>\<Sqinter>{x \<in> L | f(x) \<le> x}\<close> is a fixpoint
+  of \<open>f\<close>.
 
-  \<^bold>\<open>Proof.\<close> Let \<open>H = {x \<in> L | f(x) \<le> x}\<close> and \<open>a = \<Sqinter>H\<close>. For all \<open>x \<in> H\<close> we
-  have \<open>a \<le> x\<close>, so \<open>f(a) \<le> f(x) \<le> x\<close>. Thus \<open>f(a)\<close> is a lower bound of \<open>H\<close>,
-  whence \<open>f(a) \<le> a\<close>. We now use this inequality to prove the reverse one (!)
-  and thereby complete the proof that \<open>a\<close> is a fixpoint. Since \<open>f\<close> is
+  \<^bold>\<open>Proof.\<close> Let \<open>H = {x \<in> L | f(x) \<le> x}\<close> and \<open>a = \<Sqinter>H\<close>. For all \<open>x \<in> H\<close> we have
+  \<open>a \<le> x\<close>, so \<open>f(a) \<le> f(x) \<le> x\<close>. Thus \<open>f(a)\<close> is a lower bound of \<open>H\<close>, whence
+  \<open>f(a) \<le> a\<close>. We now use this inequality to prove the reverse one (!) and
+  thereby complete the proof that \<open>a\<close> is a fixpoint. Since \<open>f\<close> is
   order-preserving, \<open>f(f(a)) \<le> f(a)\<close>. This says \<open>f(a) \<in> H\<close>, so \<open>a \<le> f(a)\<close>.\<close>
 
 
 subsection \<open>Formal versions\<close>
 
-text \<open>The Isar proof below closely follows the original presentation.
-  Virtually all of the prose narration has been rephrased in terms of formal
-  Isar language elements. Just as many textbook-style proofs, there is a
-  strong bias towards forward proof, and several bends in the course of
-  reasoning.\<close>
+text \<open>
+  The Isar proof below closely follows the original presentation. Virtually
+  all of the prose narration has been rephrased in terms of formal Isar
+  language elements. Just as many textbook-style proofs, there is a strong
+  bias towards forward proof, and several bends in the course of reasoning.
+\<close>
 
 theorem Knaster_Tarski:
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
@@ -64,15 +66,17 @@
   qed
 qed
 
-text \<open>Above we have used several advanced Isar language elements, such as
-  explicit block structure and weak assumptions. Thus we have mimicked the
-  particular way of reasoning of the original text.
+text \<open>
+  Above we have used several advanced Isar language elements, such as explicit
+  block structure and weak assumptions. Thus we have mimicked the particular
+  way of reasoning of the original text.
 
   In the subsequent version the order of reasoning is changed to achieve
   structured top-down decomposition of the problem at the outer level, while
   only the inner steps of reasoning are done in a forward manner. We are
   certainly more at ease here, requiring only the most basic features of the
-  Isar language.\<close>
+  Isar language.
+\<close>
 
 theorem Knaster_Tarski':
   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -9,8 +9,10 @@
 imports Main
 begin
 
-text \<open>The Mutilated Checker Board Problem, formalized inductively. See @{cite
-  "paulson-mutilated-board"} for the original tactic script version.\<close>
+text \<open>
+  The Mutilated Checker Board Problem, formalized inductively. See @{cite
+  "paulson-mutilated-board"} for the original tactic script version.
+\<close>
 
 subsection \<open>Tilings\<close>
 
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Peirce.thy
--- a/src/HOL/Isar_Examples/Peirce.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Peirce.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Isar_Examples/Peirce.thy
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Makarius
 *)
 
 section \<open>Peirce's Law\<close>
@@ -8,15 +8,16 @@
 imports Main
 begin
 
-text \<open>We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently
-  non-intuitionistic statement, so its proof will certainly involve some
-  form of classical contradiction.
+text \<open>
+  We consider Peirce's Law: \<open>((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A\<close>. This is an inherently
+  non-intuitionistic statement, so its proof will certainly involve some form
+  of classical contradiction.
 
   The first proof is again a well-balanced combination of plain backward and
   forward reasoning. The actual classical step is where the negated goal may
   be introduced as additional assumption. This eventually leads to a
-  contradiction.\footnote{The rule involved there is negation elimination;
-  it holds in intuitionistic logic as well.}\<close>
+  contradiction.\<^footnote>\<open>The rule involved there is negation elimination; it holds in
+  intuitionistic logic as well.\<close>\<close>
 
 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
@@ -33,17 +34,19 @@
   qed
 qed
 
-text \<open>In the subsequent version the reasoning is rearranged by means of
-  ``weak assumptions'' (as introduced by \isacommand{presume}). Before
-  assuming the negated goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put
-  into place in order to solve the main problem. Nevertheless, we do not get
-  anything for free, but have to establish \<open>A \<longrightarrow> B\<close> later on. The overall
-  effect is that of a logical \<^emph>\<open>cut\<close>.
+text \<open>
+  In the subsequent version the reasoning is rearranged by means of ``weak
+  assumptions'' (as introduced by \<^theory_text>\<open>presume\<close>). Before assuming the negated
+  goal \<open>\<not> A\<close>, its intended consequence \<open>A \<longrightarrow> B\<close> is put into place in order to
+  solve the main problem. Nevertheless, we do not get anything for free, but
+  have to establish \<open>A \<longrightarrow> B\<close> later on. The overall effect is that of a logical
+  \<^emph>\<open>cut\<close>.
 
-  Technically speaking, whenever some goal is solved by \isacommand{show} in
-  the context of weak assumptions then the latter give rise to new subgoals,
-  which may be established separately. In contrast, strong assumptions (as
-  introduced by \isacommand{assume}) are solved immediately.\<close>
+  Technically speaking, whenever some goal is solved by \<^theory_text>\<open>show\<close> in the context
+  of weak assumptions then the latter give rise to new subgoals, which may be
+  established separately. In contrast, strong assumptions (as introduced by
+  \<^theory_text>\<open>assume\<close>) are solved immediately.
+\<close>
 
 theorem "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
 proof
@@ -62,20 +65,22 @@
   qed
 qed
 
-text \<open>Note that the goals stemming from weak assumptions may be even left
-  until qed time, where they get eventually solved ``by assumption'' as
-  well. In that case there is really no fundamental difference between the
-  two kinds of assumptions, apart from the order of reducing the individual
-  parts of the proof configuration.
+text \<open>
+  Note that the goals stemming from weak assumptions may be even left until
+  qed time, where they get eventually solved ``by assumption'' as well. In
+  that case there is really no fundamental difference between the two kinds of
+  assumptions, apart from the order of reducing the individual parts of the
+  proof configuration.
 
-  Nevertheless, the ``strong'' mode of plain assumptions is quite important
-  in practice to achieve robustness of proof text interpretation. By forcing
-  both the conclusion \<^emph>\<open>and\<close> the assumptions to unify with the pending goal
-  to be solved, goal selection becomes quite deterministic. For example,
-  decomposition with rules of the ``case-analysis'' type usually gives rise
-  to several goals that only differ in there local contexts. With strong
+  Nevertheless, the ``strong'' mode of plain assumptions is quite important in
+  practice to achieve robustness of proof text interpretation. By forcing both
+  the conclusion \<^emph>\<open>and\<close> the assumptions to unify with the pending goal to be
+  solved, goal selection becomes quite deterministic. For example,
+  decomposition with rules of the ``case-analysis'' type usually gives rise to
+  several goals that only differ in there local contexts. With strong
   assumptions these may be still solved in any order in a predictable way,
-  while weak ones would quickly lead to great confusion, eventually
-  demanding even some backtracking.\<close>
+  while weak ones would quickly lead to great confusion, eventually demanding
+  even some backtracking.
+\<close>
 
 end
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Puzzle.thy
--- a/src/HOL/Isar_Examples/Puzzle.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Puzzle.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -4,12 +4,14 @@
 imports Main
 begin
 
-text_raw \<open>\footnote{A question from ``Bundeswettbewerb Mathematik''.
-  Original pen-and-paper proof due to Herbert Ehler; Isabelle tactic
-  script by Tobias Nipkow.}\<close>
+text_raw \<open>\<^footnote>\<open>A question from ``Bundeswettbewerb Mathematik''. Original
+  pen-and-paper proof due to Herbert Ehler; Isabelle tactic script by Tobias
+  Nipkow.\<close>\<close>
 
-text \<open>\<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that
-  \<open>f (f n) < f (Suc n)\<close> for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.\<close>
+text \<open>
+  \<^bold>\<open>Problem.\<close> Given some function \<open>f: \<nat> \<rightarrow> \<nat>\<close> such that \<open>f (f n) < f (Suc n)\<close>
+  for all \<open>n\<close>. Demonstrate that \<open>f\<close> is the identity.
+\<close>
 
 theorem
   assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Summation.thy
--- a/src/HOL/Isar_Examples/Summation.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
 (*  Title:      HOL/Isar_Examples/Summation.thy
-    Author:     Markus Wenzel
+    Author:     Makarius
 *)
 
 section \<open>Summing natural numbers\<close>
@@ -8,17 +8,19 @@
 imports Main
 begin
 
-text \<open>Subsequently, we prove some summation laws of natural numbers
-  (including odds, squares, and cubes). These examples demonstrate how plain
-  natural deduction (including induction) may be combined with calculational
-  proof.\<close>
+text \<open>
+  Subsequently, we prove some summation laws of natural numbers (including
+  odds, squares, and cubes). These examples demonstrate how plain natural
+  deduction (including induction) may be combined with calculational proof.
+\<close>
 
 
 subsection \<open>Summation laws\<close>
 
-text \<open>The sum of natural numbers \<open>0 + \<cdots> + n\<close> equals \<open>n \<times> (n + 1)/2\<close>.
-  Avoiding formal reasoning about division we prove this equation multiplied
-  by \<open>2\<close>.\<close>
+text \<open>
+  The sum of natural numbers \<open>0 + \<cdots> + n\<close> equals \<open>n \<times> (n + 1)/2\<close>. Avoiding
+  formal reasoning about division we prove this equation multiplied by \<open>2\<close>.
+\<close>
 
 theorem sum_of_naturals:
   "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
@@ -35,39 +37,38 @@
     by simp
 qed
 
-text \<open>The above proof is a typical instance of mathematical induction. The
-  main statement is viewed as some \<open>?P n\<close> that is split by the induction
-  method into base case \<open>?P 0\<close>, and step case \<open>?P n \<Longrightarrow> ?P (Suc n)\<close> for
-  arbitrary \<open>n\<close>.
+text \<open>
+  The above proof is a typical instance of mathematical induction. The main
+  statement is viewed as some \<open>?P n\<close> that is split by the induction method
+  into base case \<open>?P 0\<close>, and step case \<open>?P n \<Longrightarrow> ?P (Suc n)\<close> for arbitrary \<open>n\<close>.
 
   The step case is established by a short calculation in forward manner.
   Starting from the left-hand side \<open>?S (n + 1)\<close> of the thesis, the final
   result is achieved by transformations involving basic arithmetic reasoning
-  (using the Simplifier). The main point is where the induction hypothesis
-  \<open>?S n = n \<times> (n + 1)\<close> is introduced in order to replace a certain subterm.
-  So the ``transitivity'' rule involved here is actual \<^emph>\<open>substitution\<close>. Also
-  note how the occurrence of ``\dots'' in the subsequent step documents the
-  position where the right-hand side of the hypothesis got filled in.
+  (using the Simplifier). The main point is where the induction hypothesis \<open>?S
+  n = n \<times> (n + 1)\<close> is introduced in order to replace a certain subterm. So the
+  ``transitivity'' rule involved here is actual \<^emph>\<open>substitution\<close>. Also note how
+  the occurrence of ``\dots'' in the subsequent step documents the position
+  where the right-hand side of the hypothesis got filled in.
 
   \<^medskip>
   A further notable point here is integration of calculations with plain
   natural deduction. This works so well in Isar for two reasons.
 
-    \<^enum> Facts involved in \isakeyword{also}~/ \isakeyword{finally}
-    calculational chains may be just anything. There is nothing special
-    about \isakeyword{have}, so the natural deduction element
-    \isakeyword{assume} works just as well.
+    \<^enum> Facts involved in \<^theory_text>\<open>also\<close>~/ \<^theory_text>\<open>finally\<close> calculational chains may be just
+    anything. There is nothing special about \<^theory_text>\<open>have\<close>, so the natural deduction
+    element \<^theory_text>\<open>assume\<close> works just as well.
   
     \<^enum> There are two \<^emph>\<open>separate\<close> primitives for building natural deduction
-    contexts: \isakeyword{fix}~\<open>x\<close> and \isakeyword{assume}~\<open>A\<close>. Thus it is
-    possible to start reasoning with some new ``arbitrary, but fixed''
-    elements before bringing in the actual assumption. In contrast, natural
-    deduction is occasionally formalized with basic context elements of the
-    form \<open>x:A\<close> instead.
+    contexts: \<^theory_text>\<open>fix x\<close> and \<^theory_text>\<open>assume A\<close>. Thus it is possible to start reasoning
+    with some new ``arbitrary, but fixed'' elements before bringing in the
+    actual assumption. In contrast, natural deduction is occasionally
+    formalized with basic context elements of the form \<open>x:A\<close> instead.
 
   \<^medskip>
   We derive further summation laws for odds, squares, and cubes as follows.
-  The basic technique of induction plus calculation is the same as before.\<close>
+  The basic technique of induction plus calculation is the same as before.
+\<close>
 
 theorem sum_of_odds:
   "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
@@ -85,8 +86,10 @@
     by simp
 qed
 
-text \<open>Subsequently we require some additional tweaking of Isabelle built-in
-  arithmetic simplifications, such as bringing in distributivity by hand.\<close>
+text \<open>
+  Subsequently we require some additional tweaking of Isabelle built-in
+  arithmetic simplifications, such as bringing in distributivity by hand.
+\<close>
 
 lemmas distrib = add_mult_distrib add_mult_distrib2
 
@@ -123,15 +126,17 @@
     by simp
 qed
 
-text \<open>Note that in contrast to older traditions of tactical proof
-  scripts, the structured proof applies induction on the original,
-  unsimplified statement. This allows to state the induction cases robustly
-  and conveniently. Simplification (or other automated) methods are then
-  applied in terminal position to solve certain sub-problems completely.
+text \<open>
+  Note that in contrast to older traditions of tactical proof scripts, the
+  structured proof applies induction on the original, unsimplified statement.
+  This allows to state the induction cases robustly and conveniently.
+  Simplification (or other automated) methods are then applied in terminal
+  position to solve certain sub-problems completely.
 
   As a general rule of good proof style, automatic methods such as \<open>simp\<close> or
-  \<open>auto\<close> should normally be never used as initial proof methods with a
-  nested sub-proof to address the automatically produced situation, but only
-  as terminal ones to solve sub-problems.\<close>
+  \<open>auto\<close> should normally be never used as initial proof methods with a nested
+  sub-proof to address the automatically produced situation, but only as
+  terminal ones to solve sub-problems.
+\<close>
 
 end
diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/document/root.tex
--- a/src/HOL/Isar_Examples/document/root.tex	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/document/root.tex	Sat Dec 26 15:44:14 2015 +0100
@@ -16,7 +16,7 @@
 \begin{document}
 
 \title{Miscellaneous Isabelle/Isar examples for Higher-Order Logic}
-\author{Markus Wenzel \\[2ex]
+\author{Makarius Wenzel \\[2ex]
   With contributions by Gertrud Bauer and Tobias Nipkow}
 \maketitle