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_Total_EX2.thy
changeset 80914 d97fdabd9e2b
parent 74500 40f03761f77f 
--- a/src/HOL/IMP/VCG_Total_EX2.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/IMP/VCG_Total_EX2.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -16,14 +16,14 @@
 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) |
+  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 assn2 lvname bexp acom
-    ("({_'/_}/ WHILE _/ DO _)"  [0, 0, 0, 61] 61)
+    (\<open>({_'/_}/ WHILE _/ DO _)\<close>  [0, 0, 0, 61] 61)
 
-notation com.SKIP ("SKIP")
+notation com.SKIP (\<open>SKIP\<close>)
 
 text\<open>Strip annotations:\<close>
isabelle