# HG changeset patch
# User nipkow
# Date 1643968129 -3600
# Node ID 988d7c7e2254c6044698280b8201ea3a434c6b2d
# Parent  57df04e4f018a9b040328b22aa663035888e50d2
tuned output syntax: Hoare triples are now blocks

diff -r 57df04e4f018 -r 988d7c7e2254 src/HOL/Hoare/Hoare_Syntax.thy
--- a/src/HOL/Hoare/Hoare_Syntax.thy	Thu Feb 03 10:33:55 2022 +0100
+++ b/src/HOL/Hoare/Hoare_Syntax.thy	Fri Feb 04 10:48:49 2022 +0100
@@ -32,8 +32,8 @@
  "_hoare_vars" :: "[idts, 'assn,'com, 'assn] \<Rightarrow> bool"  ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
  "_hoare_vars_tc" :: "[idts, 'assn, 'com, 'assn] \<Rightarrow> bool"  ("VARS _// [_] // _ // [_]" [0,0,55,0] 50)
 syntax (output)
- "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool"  ("{_} // _ // {_}" [0,55,0] 50)
- "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool"  ("[_] // _ // [_]" [0,55,0] 50)
+ "_hoare" :: "['assn, 'com, 'assn] \<Rightarrow> bool"  ("({_} // _ // {_})" [0,55,0] 50)
+ "_hoare_tc" :: "['assn, 'com, 'assn] \<Rightarrow> bool"  ("([_] // _ // [_])" [0,55,0] 50)
 
 text \<open>Completeness requires(?) the ability to refer to an outer variant in an inner invariant.
 Thus we need to abstract over a variable equated with the variant, the \<open>x\<close> in \<open>VAR {x = t}\<close>.