Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IMP/VCG.thy
changeset 80914 d97fdabd9e2b
parent 68776 403dd13cf6e9 
--- a/src/HOL/IMP/VCG.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/IMP/VCG.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -9,13 +9,13 @@
 text\<open>Commands where loops are annotated with invariants.\<close>
 
 datatype acom =
-  Askip                  ("SKIP") |
-  Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
-  Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |
-  Aif bexp acom acom     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61) |
-  Awhile assn bexp acom  ("({_}/ WHILE _/ DO _)"  [0, 0, 61] 61)
+  Askip                  (\<open>SKIP\<close>) |
+  Aassign vname aexp     (\<open>(_ ::= _)\<close> [1000, 61] 61) |
+  Aseq   acom acom       (\<open>_;;/ _\<close>  [60, 61] 60) |
+  Aif bexp acom acom     (\<open>(IF _/ THEN _/ ELSE _)\<close>  [0, 0, 61] 61) |
+  Awhile assn bexp acom  (\<open>({_}/ WHILE _/ DO _)\<close>  [0, 0, 61] 61)
 
-notation com.SKIP ("SKIP")
+notation com.SKIP (\<open>SKIP\<close>)
 
 text\<open>Strip annotations:\<close>
isabelle