src/HOL/Hoare/Hoare.thy

  'a com = Basic "'a \<Rightarrow> 'a"         
    | Seq "'a com" "'a com"               ("(_;/ _)"      [61,60] 60)
    | Cond "'a bexp" "'a com" "'a com"    ("(1IF _/ THEN _ / ELSE _/ FI)"  [0,0,0] 61)
    | While "'a bexp" "'a assn" "'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
   
-syntax
-  "@assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
-  "@annskip" :: "'a com"                    ("SKIP")
-
-translations
-            "SKIP" == "Basic id"
+abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 types 'a sem = "'a => 'a => bool"
 
 consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
 primrec

 
 constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
   "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
 
 
+
+(** parse translations **)
+
 syntax
- "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+  "_assign"  :: "id => 'b => 'a com"        ("(2_ :=/ _)" [70,65] 61)
+
+syntax
+ "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
 syntax ("" output)
- "@hoare"      :: "['a assn,'a com,'a assn] => bool"
+ "_hoare"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
-
-(** parse translations **)
-
-ML{*
+ML {*
 
 local
 
 fun abs((a,T),body) =
   let val a = absfree(a, dummyT, body)

   
 fun assn_tr r xs = Syntax.const "Collect" $ mk_abstuple xs r;
 *}
 (* com_tr *)
 ML{*
-fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
+fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
       Syntax.const "Basic" $ mk_fexp a e xs
   | com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
   | com_tr (Const ("Seq",_) $ c1 $ c2) xs =
       Syntax.const "Seq" $ com_tr c1 xs $ com_tr c2 xs
   | com_tr (Const ("Cond",_) $ b $ c1 $ c2) xs =

       end
   | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts);
 end
 *}
 
-parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
 
 
 (*****************************************************************************)
 
 (*** print translations ***)

 (*com_tr' *)
 ML{*
 fun mk_assign f =
   let val (vs, ts) = mk_vts f;
       val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
-  in if ch then Syntax.const "@assign" $ fst(which) $ snd(which)
-     else Syntax.const "@skip" end;
+  in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
+     else Syntax.const @{const_syntax annskip} end;
 
 fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
                                            else Syntax.const "Basic" $ f
   | com_tr' (Const ("Seq",_) $ c1 $ c2) = Syntax.const "Seq" $
                                                  com_tr' c1 $ com_tr' c2

                                                bexp_tr' b $ assn_tr' I $ com_tr' c
   | com_tr' t = t;
 
 
 fun spec_tr' [p, c, q] =
-  Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
-*}
-
-print_translation {* [("Valid", spec_tr')] *}
+  Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+*}
+
+print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
 
 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
 by (auto simp:Valid_def)
 
 lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"