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/Example.thy
changeset 77645 7edbb16bc60f
parent 68451 c34aa23a1fb6 
--- a/src/HOL/MicroJava/J/Example.thy	Tue Mar 14 14:00:07 2023 +0100
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Mar 14 18:19:10 2023 +0100
@@ -120,11 +120,11 @@
 
 abbreviation
   obj1  :: obj where
-  "obj1 == (Ext, Map.empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
+  "obj1 == (Ext, Map.empty((vee, Base)\<mapsto>Bool False, (vee, Ext )\<mapsto>Intg 0))"
 
 abbreviation "s0 == Norm    (Map.empty, Map.empty)"
 abbreviation "s1 == Norm    (Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))"
-abbreviation "s2 == Norm    (Map.empty(a\<mapsto>obj1),Map.empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+abbreviation "s2 == Norm    (Map.empty(a\<mapsto>obj1),Map.empty(x\<mapsto>Null, This\<mapsto>Addr a))"
 abbreviation "s3 == (Some NP, Map.empty(a\<mapsto>obj1),Map.empty(e\<mapsto>Addr a))"
 
 lemmas map_of_Cons = map_of.simps(2)
isabelle