--- a/src/HOL/Isar_examples/HoareEx.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Isar_examples/HoareEx.thy Sat Oct 06 00:02:46 2001 +0200
@@ -39,7 +39,7 @@
*}
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 {*
@@ -49,13 +49,13 @@
``obvious'' consequences as well.
*}
-lemma "|- .{True}. \<acute>N := # 10 .{\<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}."
+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 "|- .{\<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}."