src/HOL/Hoare/Hoare_Logic_Abort.thy

 | Abort
 | 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 var" "'a com"  ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)"  [0,0,0,0] 61)
 
-syntax (xsymbols)
+syntax
   "_whilePC" :: "'a bexp \<Rightarrow> 'a assn \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(1WHILE _/ INV {_} //DO _ /OD)"  [0,0,0] 61)
-
 translations
-  "WHILE b INV {x} DO c OD" => "WHILE b INV {x} VAR {0} DO c OD"
+  "WHILE b INV {x} DO c OD" \<rightharpoonup> "WHILE b INV {x} VAR {0} DO c OD"
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
 type_synonym 'a sem = "'a option => 'a option => bool"
 

   "_assign" :: "idt => 'b => 'a com"  ("(2_ :=/ _)" [70, 65] 61)
 
 syntax
   "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax ("" output)
+syntax (output)
   "_hoare_abort"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
 
 ML_file \<open>hoare_syntax.ML\<close>
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_vars\<close>, K Hoare_Syntax.hoare_vars_tr)]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>Valid\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort\<close>))]\<close>
 
 syntax
  "_hoare_abort_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                           ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
-syntax ("" output)
+syntax (output)
  "_hoare_abort_tc"      :: "['a assn,'a com,'a assn] => bool"
                           ("[_] // _ // [_]" [0,55,0] 50)
 
 parse_translation \<open>[(\<^syntax_const>\<open>_hoare_abort_tc_vars\<close>, K Hoare_Syntax.hoare_tc_vars_tr)]\<close>
 print_translation \<open>[(\<^const_syntax>\<open>ValidTC\<close>, K (Hoare_Syntax.spec_tr' \<^syntax_const>\<open>_hoare_abort_tc\<close>))]\<close>