Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned output syntax: INV and VAR are now blocks
authornipkow
Thu, 03 Feb 2022 10:33:55 +0100
changeset 75061 57df04e4f018
parent 75060 789e0e1a9e33
child 75062 988d7c7e2254
tuned output syntax: INV and VAR are now blocks
src/HOL/Hoare/Hoare_Syntax.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Hoare/Hoare_Syntax.thy	Wed Feb 02 13:43:48 2022 +0100
+++ b/src/HOL/Hoare/Hoare_Syntax.thy	Thu Feb 03 10:33:55 2022 +0100
@@ -13,7 +13,7 @@
   "_assign" :: "idt \<Rightarrow> 'b \<Rightarrow> 'com"  ("(2_ :=/ _)" [70, 65] 61)
   "_Seq" :: "'com \<Rightarrow> 'com \<Rightarrow> 'com"  ("(_;/ _)" [61,60] 60)
   "_Cond" :: "'bexp \<Rightarrow> 'com \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
-  "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1WHILE _/ INV {_} / VAR {_} //DO _ /OD)" [0,0,0,0] 61)
+  "_While" :: "'bexp \<Rightarrow> 'assn \<Rightarrow> 'var \<Rightarrow> 'com \<Rightarrow> 'com"  ("(1WHILE _/ INV {(_)} / VAR {(_)} //DO _ /OD)" [0,0,0,0] 61)
 
 text \<open>The \<open>VAR {_}\<close> syntax supports two variants:
 \<^item> \<open>VAR {x = t}\<close> where \<open>t::nat\<close> is the decreasing expression,
isabelle