Mercurial Mercurial > repos > isabelle / comparison
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/State.thy
changeset 61169 4de9ff3ea29a
parent 58886 8a6cac7c7247
child 61361 8b5f00202e1a
equal deleted inserted replaced
61168:dcdfb6355a05 61169:4de9ff3ea29a 
   189 
   189 
   190 instantiation loc' :: equal
 
   190 instantiation loc' :: equal
 
   191 begin
 
   191 begin
 
   192 
   192 
   193 definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
 
   193 definition "HOL.equal (l :: loc') l' \<longleftrightarrow> l = l'"
 
   194 instance by default (simp add: equal_loc'_def)
 
   194 instance by standard (simp add: equal_loc'_def)
 
   195 
   195 
   196 end
 
   196 end
 
   197 
   197 
   198 end
 
   198 end
isabelle