src/HOL/Isar_examples/HoareEx.thy

 text {*
  Using the basic \name{assign} rule directly is a bit cumbersome.
 *}
 
 lemma
-  "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = #10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
+  "|- .{\<acute>(N_update (# 2 * \<acute>N)) : .{\<acute>N = # 10}.}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
   by (rule assign)
 
 text {*
  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.
 *}
 
-lemma "|- .{True}. \<acute>N := #10 .{\<acute>N = #10}."
-  by hoare
-
-lemma "|- .{2 * \<acute>N = #10}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
-  by hoare
-
-lemma "|- .{\<acute>N = #5}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
+lemma "|- .{True}. \<acute>N := # 10 .{\<acute>N = # 10}."
+  by hoare
+
+lemma "|- .{# 2 * \<acute>N = # 10}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
+  by hoare
+
+lemma "|- .{\<acute>N = # 5}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
   by hoare simp
 
 lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
   by hoare
 

   finally show ?thesis .
 qed
 
 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
 proof -
-  have "!!m n. m = n --> m + 1 ~= n"
+  have "!!m n::nat. m = n --> m + 1 ~= n"
       -- {* inclusion of assertions expressed in ``pure'' logic, *}
       -- {* without mentioning the state space *}
     by simp
   also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
     by hoare