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/MicroJava/J/Conform.thy
changeset 67443 3abf6a722518
parent 62042 6c6ccf573479 
--- a/src/HOL/MicroJava/J/Conform.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -7,7 +7,7 @@
 
 theory Conform imports State WellType Exceptions begin
 
-type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  \<comment> "same as \<open>env\<close> of \<open>WellType.thy\<close>"
+type_synonym 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  \<comment> \<open>same as \<open>env\<close> of \<open>WellType.thy\<close>\<close>
 
 definition hext :: "aheap => aheap => bool" ("_ \<le>| _" [51,51] 50) where
  "h\<le>|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
isabelle