1.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Tue Oct 20 19:37:09 2009 +0200
     1.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -228,11 +228,11 @@
     1.4    "_Assert"      :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
     1.5  
     1.6  translations
     1.7 -  ".{b}."                   => "Collect .(b)."
     1.8 +  ".{b}."                   => "CONST Collect .(b)."
     1.9    "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
    1.10 -  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
    1.11 -  "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
    1.12 -  "WHILE b INV i DO c OD"   => "While .{b}. i c"
    1.13 +  "\<acute>x := a"                 => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
    1.14 +  "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
    1.15 +  "WHILE b INV i DO c OD"   => "CONST While .{b}. i c"
    1.16    "WHILE b DO c OD"         == "WHILE b INV CONST undefined DO c OD"
    1.17  
    1.18  parse_translation {*