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/NanoJava/Decl.thy
changeset 67443 3abf6a722518
parent 63167 0909deb8059b 
--- a/src/HOL/NanoJava/Decl.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/NanoJava/Decl.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -8,8 +8,8 @@
 theory Decl imports Term begin
 
 datatype ty
-  = NT           \<comment>\<open>null type\<close>
-  | Class cname  \<comment>\<open>class type\<close>
+  = NT           \<comment> \<open>null type\<close>
+  | Class cname  \<comment> \<open>class type\<close>
 
 text\<open>Field declaration\<close>
 type_synonym fdecl           
@@ -45,9 +45,9 @@
   (type) "prog " \<leftharpoondown> (type) "cdecl list"
 
 axiomatization
-  Prog    :: prog       \<comment>\<open>program as a global value\<close>
+  Prog    :: prog       \<comment> \<open>program as a global value\<close>
 and
-  Object  :: cname      \<comment>\<open>name of root class\<close>
+  Object  :: cname      \<comment> \<open>name of root class\<close>
 
 
 definition "class" :: "cname \<rightharpoonup> class" where
isabelle