diff -r f92bf6674699 -r 846c72206207 src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 11:43:02 2015 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Mon Nov 02 13:58:19 2015 +0100
@@ -13,10 +13,9 @@
 
 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 @{text I},
-  @{text K}, and @{text S}.  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
@@ -51,14 +50,12 @@
   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.
+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>
+  First of all, proof by assumption may be abbreviated as a single dot.\<close>
 
 lemma "A \<longrightarrow> A"
 proof
@@ -66,21 +63,21 @@
   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>
+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>
 
 lemma "A \<longrightarrow> A"
 proof
 qed
 
-text \<open>Note that the \isacommand{proof} command refers to the @{text
-  rule} 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 \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>
 
 lemma "A \<longrightarrow> A"
   by rule
@@ -89,19 +86,18 @@
 
 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.}\<close>
+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>Let us also reconsider @{text K}.  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.
+  \<^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.
 
-  The @{text intro} proof method repeatedly decomposes a goal's
-  conclusion.\footnote{The dual method is @{text elim}, acting on a
-  goal's premises.}\<close>
+  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>
 
 lemma "A \<longrightarrow> B \<longrightarrow> A"
 proof (intro impI)
@@ -114,29 +110,27 @@
 lemma "A \<longrightarrow> B \<longrightarrow> A"
   by (intro impI)
 
-text \<open>Just like @{text rule}, the @{text intro} and @{text elim}
-  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, @{text intro} and @{text elim} would be typically
-  restricted to certain structures by giving a few rules only, e.g.\
-  \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
-  and universal quantifiers.
+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.
 
-  Such well-tuned iterated decomposition of certain structures is the
-  prime application of @{text intro} and @{text elim}.  In contrast,
-  terminal steps that solve a goal completely are usually performed by
-  actual automated proof methods (such as \isacommand{by}~@{text
-  blast}.\<close>
+  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>
 
 
 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 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 @{text "A \<and> B \<longrightarrow> B \<and> A"}.
+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>
 
@@ -150,13 +144,12 @@
   qed
 qed
 
-text \<open>Above, the @{text "conjunct_1/2"} projection rules had to be
-  named explicitly, since the goals @{text B} and @{text A} did not
-  provide any structural clue.  This may be avoided using
-  \isacommand{from} to focus on the @{text "A \<and> B"} assumption as the
-  current facts, enabling the use of double-dot proofs.  Note that
-  \isacommand{from} already does forward-chaining, involving the
-  @{text conjE} 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 \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>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
@@ -168,27 +161,26 @@
   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 @{text "B \<and> A"}
-  from @{text "A \<and> B"} actually becomes an elimination, rather than an
-  introduction.  The resulting proof structure directly corresponds to
-  that of the @{text conjE} rule, including the repeated goal
-  proposition that is abbreviated as @{text ?thesis} 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
+  \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>
 
 lemma "A \<and> B \<longrightarrow> B \<and> A"
 proof
   assume "A \<and> B"
   then show "B \<and> A"
-  proof                    -- \<open>rule @{text conjE} of @{text "A \<and> B"}\<close>
+  proof                    -- \<open>rule \<open>conjE\<close> of \<open>A \<and> B\<close>\<close>
     assume B A
-    then show ?thesis ..   -- \<open>rule @{text conjI} of @{text "B \<and> A"}\<close>
+    then show ?thesis ..   -- \<open>rule \<open>conjI\<close> of \<open>B \<and> A\<close>\<close>
   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
@@ -198,9 +190,9 @@
   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 ``-'' 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 -
@@ -210,27 +202,28 @@
     from \<open>A \<and> B\<close> have B ..
     from \<open>B\<close> \<open>A\<close> have "B \<and> A" ..
   }
-  then show ?thesis ..         -- \<open>rule @{text impI}\<close>
+  then show ?thesis ..         -- \<open>rule \<open>impI\<close>\<close>
 qed
 
-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).
+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).
 
-  The general lesson learned here is that good proof style would
-  achieve just the \emph{right} 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.\<close>
+  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.
 
-text \<open>For our example the most appropriate way of reasoning is
-  probably the middle one, with conjunction introduction done after
-  elimination.\<close>
+  \<^medskip>
+  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
@@ -246,22 +239,22 @@
 
 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 @{text "P \<or> P \<longrightarrow> P"}.  The proof
-  below involves forward-chaining from @{text "P \<or> P"}, followed by an
-  explicit case-analysis on the two \emph{identical} 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
   assume "P \<or> P"
   then show P
   proof                    -- \<open>
-    rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
+    rule \<open>disjE\<close>: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
 \<close>
     assume P show P by fact
   next
@@ -269,27 +262,27 @@
   qed
 qed
 
-text \<open>Case splits are \emph{not} 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 \isacommand{next} 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 ``cases'', i.e.\ new subgoals with individual local
-  assumptions.  The corresponding proof text typically mimics this by
-  establishing results in appropriate contexts, separated by blocks.
+  \<^medskip>
+  In general, applying proof methods may split up a goal into separate
+  ``cases'', i.e.\ new subgoals with individual local assumptions. The
+  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 behavior 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{not} require \isacommand{next} to separate the subsequent step
-  case.
+  \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.
 
-  \medskip In our example the situation is even simpler, since the two
-  cases actually coincide.  Consequently the proof may be rephrased as
-  follows.\<close>
+  \<^medskip>
+  In our example the situation is even simpler, since the two cases actually
+  coincide. Consequently the proof may be rephrased as follows.\<close>
 
 lemma "P \<or> P \<longrightarrow> P"
 proof
@@ -316,37 +309,34 @@
 
 subsubsection \<open>A quantifier proof\<close>
 
-text \<open>To illustrate quantifier reasoning, let us prove @{text
-  "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"}.  Informally, this holds because any
-  @{text a} with @{text "P (f a)"} may be taken as a witness for the
-  second existential statement.
+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>
+  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>
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
   assume "\<exists>x. P (f x)"
   then show "\<exists>y. P y"
-  proof (rule exE)             -- \<open>
-    rule @{text exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
-\<close>
+  proof (rule exE)             --
+    \<open>rule \<open>exE\<close>: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}\<close>
     fix a
     assume "P (f a)" (is "P ?witness")
     then show ?thesis by (rule exI [of P ?witness])
   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
@@ -359,10 +349,9 @@
   qed
 qed
 
-text \<open>Explicit @{text \<exists>}-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 ``\isakeyword{obtain}''
+  provides a more handsome way to do generalized existence reasoning.\<close>
 
 lemma "(\<exists>x. P (f x)) \<longrightarrow> (\<exists>y. P y)"
 proof
@@ -371,21 +360,19 @@
   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{not} refer
-  to the parameters introduced there.\<close>
+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>
 
 
 subsubsection \<open>Deriving rules in Isabelle\<close>
 
-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>
+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>
 
 theorem conjE: "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> C) \<Longrightarrow> C"
 proof -