src/HOL/Isar_examples/Hoare.thy
changeset 22759 e4a3f49eb924
parent 22741 4bd02e03305c
child 24472 943ef707396c
     1.1 --- a/src/HOL/Isar_examples/Hoare.thy	Fri Apr 20 17:58:24 2007 +0200
     1.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Fri Apr 20 17:58:25 2007 +0200
     1.3 @@ -228,8 +228,8 @@
     1.4  
     1.5  translations
     1.6    ".{b}."                   => "Collect .(b)."
     1.7 -  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (CONST K_record a)) \<in> B}."
     1.8 -  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (CONST K_record a)))."
     1.9 +  "B [a/\<acute>x]"                => ".{\<acute>(_update_name x (K_record a)) \<in> B}."
    1.10 +  "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (K_record 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    "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
    1.14 @@ -270,7 +270,7 @@
    1.15        | update_name_tr' (Const x) = Const (upd_tr' x)
    1.16        | update_name_tr' _ = raise Match;
    1.17  
    1.18 -    fun assign_tr' (Abs (x, _, f $ (Const ("K_record",_)$t) $ Bound 0) :: ts) =
    1.19 +    fun assign_tr' (Abs (x, _, f $ (Const (@{const_syntax "K_record"},_)$t) $ Bound 0) :: ts) =
    1.20            quote_tr' (Syntax.const "_Assign" $ update_name_tr' f)
    1.21              (Abs (x, dummyT, t) :: ts)
    1.22        | assign_tr' _ = raise Match;
    1.23 @@ -448,7 +448,7 @@
    1.24  method_setup hoare = {*
    1.25    Method.no_args
    1.26      (Method.SIMPLE_METHOD'
    1.27 -       (hoare_tac (simp_tac (HOL_basic_ss addsimps [thm "Record.K_record_apply"] )))) *}
    1.28 +       (hoare_tac (simp_tac (HOL_basic_ss addsimps [@{thm "Record.K_record_apply"}] )))) *}
    1.29    "verification condition generator for Hoare logic"
    1.30  
    1.31  end