# HG changeset patch
# User wenzelm
# Date 1608733252 -3600
# Node ID 8e99246f89c05aeed4a087764db1e6e819511074
# Parent  a8050df4f58f6385bd4e421028bf85e514853da9
clarified syntax modes, avoid obsolete "xsymbols";

diff -r a8050df4f58f -r 8e99246f89c0 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Dec 23 15:01:50 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Dec 23 15:20:52 2020 +0100
@@ -23,11 +23,10 @@
 | 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"
 
@@ -78,7 +77,7 @@
 syntax
  "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax ("" output)
+syntax (output)
  "_hoare"      :: "['a assn,'a com,'a assn] => bool"
                  ("{_} // _ // {_}" [0,55,0] 50)
 
@@ -89,7 +88,7 @@
 syntax
  "_hoare_tc_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
                     ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
-syntax ("" output)
+syntax (output)
  "_hoare_tc"      :: "['a assn,'a com,'a assn] => bool"
                     ("[_] // _ // [_]" [0,55,0] 50)
 
diff -r a8050df4f58f -r 8e99246f89c0 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Dec 23 15:01:50 2020 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Dec 23 15:20:52 2020 +0100
@@ -21,11 +21,10 @@
 | 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"
 
@@ -80,7 +79,7 @@
 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)
 
@@ -91,7 +90,7 @@
 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)