--- a/src/HOL/Isar_Examples/Hoare.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Mon Feb 08 21:28:27 2010 +0100
@@ -228,11 +228,11 @@
"_Assert" :: "'a => 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
translations
- ".{b}." => "Collect .(b)."
+ ".{b}." => "CONST Collect .(b)."
"B [a/\<acute>x]" => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
- "\<acute>x := a" => "Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
- "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
- "WHILE b INV i DO c OD" => "While .{b}. i c"
+ "\<acute>x := a" => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
+ "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
+ "WHILE b INV i DO c OD" => "CONST While .{b}. i c"
"WHILE b DO c OD" == "WHILE b INV CONST undefined DO c OD"
parse_translation {*