diff -r f92bf6674699 -r 846c72206207 src/HOL/Isar_Examples/Hoare_Ex.thy
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy	Mon Nov 02 11:43:02 2015 +0100
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy	Mon Nov 02 13:58:19 2015 +0100
@@ -6,9 +6,9 @@
 
 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,29 +16,28 @@
   N :: nat
   S :: nat
 
-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>
+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>
 
 
 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.\<close>
 
-text \<open>Using the basic @{text assign} rule directly is a bit
+text \<open>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 simplification.  The \name{hoare} method performs the basic state
-  update for us; we may apply the Simplifier afterwards to achieve
-  ``obvious'' consequences as well.\<close>
+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>
 
 lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>"
   by hoare
@@ -67,8 +66,8 @@
       \<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
+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>
 
@@ -84,9 +83,9 @@
   oops
 
 
-text \<open>In the following assignments we make use of the consequence
-  rule in order to achieve the intended precondition.  Certainly, the
-  \name{hoare} 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 -
@@ -114,10 +113,10 @@
 
 subsection \<open>Multiplication by addition\<close>
 
-text \<open>We now do some basic examples of actual \texttt{WHILE}
-  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>
@@ -141,10 +140,10 @@
   finally show ?thesis .
 qed
 
-text \<open>The subsequent version of the proof applies the @{text hoare}
-  method to reduce the Hoare statement to a purely logical problem
-  that can be solved fully automatically.  Note that we have to
-  specify the \texttt{WHILE} 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>
@@ -157,15 +156,15 @@
 
 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.\<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>The following proof is quite explicit in the individual steps
-  taken, with the \name{hoare} 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>
+  \<^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>
 
 theorem
   "\<turnstile> \<lbrace>True\<rbrace>
@@ -203,9 +202,8 @@
   finally show ?thesis .
 qed
 
-text \<open>The next version uses the @{text hoare} 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>
@@ -230,8 +228,8 @@
   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>
@@ -248,8 +246,8 @@
 
 subsection \<open>Time\<close>
 
-text \<open>A simple embedding of time in Hoare logic: function @{text
-  timeit} 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