1.1 --- a/src/HOL/Isar_examples/HoareEx.thy	Fri Oct 05 21:50:37 2001 +0200
     1.2 +++ b/src/HOL/Isar_examples/HoareEx.thy	Fri Oct 05 21:52:39 2001 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4  *}
     1.5  
     1.6  lemma
     1.7 -  "|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = #10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
     1.8 +  "|- .{\<acute>(N_update (# 2 * \<acute>N)) : .{\<acute>N = # 10}.}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
     1.9    by (rule assign)
    1.10  
    1.11  text {*
    1.12 @@ -49,13 +49,13 @@
    1.13   ``obvious'' consequences as well.
    1.14  *}
    1.15  
    1.16 -lemma "|- .{True}. \<acute>N := #10 .{\<acute>N = #10}."
    1.17 +lemma "|- .{True}. \<acute>N := # 10 .{\<acute>N = # 10}."
    1.18    by hoare
    1.19  
    1.20 -lemma "|- .{2 * \<acute>N = #10}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
    1.21 +lemma "|- .{# 2 * \<acute>N = # 10}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
    1.22    by hoare
    1.23  
    1.24 -lemma "|- .{\<acute>N = #5}. \<acute>N := 2 * \<acute>N .{\<acute>N = #10}."
    1.25 +lemma "|- .{\<acute>N = # 5}. \<acute>N := # 2 * \<acute>N .{\<acute>N = # 10}."
    1.26    by hoare simp
    1.27  
    1.28  lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."
    1.29 @@ -112,7 +112,7 @@
    1.30  
    1.31  lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."
    1.32  proof -
    1.33 -  have "!!m n. m = n --> m + 1 ~= n"
    1.34 +  have "!!m n::nat. m = n --> m + 1 ~= n"
    1.35        -- {* inclusion of assertions expressed in ``pure'' logic, *}
    1.36        -- {* without mentioning the state space *}
    1.37      by simp