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/Metis_Examples/Trans_Closure.thy
changeset 67443 3abf6a722518
parent 63167 0909deb8059b 
--- a/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Metis_Examples/Trans_Closure.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -16,11 +16,11 @@
 type_synonym addr = nat
 
 datatype val
-  = Unit        \<comment> "dummy result value of void expressions"
-  | Null        \<comment> "null reference"
-  | Bool bool   \<comment> "Boolean value"
-  | Intg int    \<comment> "integer value"
-  | Addr addr   \<comment> "addresses of objects in the heap"
+  = Unit        \<comment> \<open>dummy result value of void expressions\<close>
+  | Null        \<comment> \<open>null reference\<close>
+  | Bool bool   \<comment> \<open>Boolean value\<close>
+  | Intg int    \<comment> \<open>integer value\<close>
+  | Addr addr   \<comment> \<open>addresses of objects in the heap\<close>
 
 consts R :: "(addr \<times> addr) set"
isabelle