1.1 --- a/src/HOL/Hoare/Hoare.thy	Thu Jul 23 18:44:09 2009 +0200
     1.2 +++ b/src/HOL/Hoare/Hoare.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -24,12 +24,7 @@
     1.4     | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
     1.5     | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
     1.6    
     1.7 -syntax
     1.8 -  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
     1.9 -  "@annskip" :: "'a com"                    ("SKIP")
    1.10 -
    1.11 -translations
    1.12 -            "SKIP" == "Basic id"
    1.13 +abbreviation annskip ("SKIP") where "SKIP == Basic id"
    1.14  
    1.15  types 'a sem = "'a => 'a => bool"
    1.16  
    1.17 @@ -50,16 +45,19 @@
    1.18    "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
    1.19  
    1.20  
    1.21 -syntax
    1.22 - "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
    1.23 -                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
    1.24 -syntax ("" output)
    1.25 - "@hoare"      :: "['a assn,'a com,'a assn] => bool"
    1.26 -                 ("{_} // _ // {_}" [0,55,0] 50)
    1.27  
    1.28  (** parse translations **)
    1.29  
    1.30 -ML{*
    1.31 +syntax
    1.32 +  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
    1.33 +
    1.34 +syntax
    1.35 + "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
    1.36 +                 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
    1.37 +syntax ("" output)
    1.38 + "_hoare"      :: "['a assn,'a com,'a assn] => bool"
    1.39 +                 ("{_} // _ // {_}" [0,55,0] 50)
    1.40 +ML {*
    1.41  
    1.42  local
    1.43  
    1.44 @@ -91,7 +89,7 @@
    1.45  *}
    1.46  (* com_tr *)
    1.47  ML{*
    1.48 -fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
    1.49 +fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
    1.50        Syntax.const "Basic" $ mk_fexp a e xs
    1.51    | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
    1.52    | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
    1.53 @@ -123,7 +121,7 @@
    1.54  end
    1.55  *}
    1.56  
    1.57 -parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
    1.58 +parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
    1.59  
    1.60  
    1.61  (*****************************************************************************)
    1.62 @@ -175,8 +173,8 @@
    1.63  fun mk_assign f =
    1.64    let val (vs, ts) = mk_vts f;
    1.65        val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
    1.66 -  in if ch then Syntax.const "@assign" $ fst(which) $ snd(which)
    1.67 -     else Syntax.const "@skip" end;
    1.68 +  in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
    1.69 +     else Syntax.const @{const_syntax annskip} end;
    1.70  
    1.71  fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
    1.72                                             else Syntax.const "Basic" $ f
    1.73 @@ -190,10 +188,10 @@
    1.74  
    1.75  
    1.76  fun spec_tr' [p, c, q] =
    1.77 -  Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
    1.78 +  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
    1.79  *}
    1.80  
    1.81 -print_translation {* [("Valid", spec_tr')] *}
    1.82 +print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
    1.83  
    1.84  lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
    1.85  by (auto simp:Valid_def)