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/AxSem.thy
changeset 11772 cf618fe8facd
parent 11565 ab004c0ecc63
child 12934 6003b4f916c0 
--- a/src/HOL/NanoJava/AxSem.thy	Sun Oct 14 22:15:07 2001 +0200
+++ b/src/HOL/NanoJava/AxSem.thy	Mon Oct 15 17:02:57 2001 +0200
@@ -79,7 +79,7 @@
 
   Call: "[| A |-e {P} e1 {Q}; \<forall>a. A |-e {Q a} e2 {R a};
     \<forall>a p ls. A |- {\<lambda>s'. \<exists>s. R a p s \<and> ls = s \<and> 
-                    s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(reset_locs s))}
+                    s' = lupd(This\<mapsto>a)(lupd(Par\<mapsto>p)(del_locs s))}
                   Meth (C,m) {\<lambda>s. S (s<Res>) (set_locs ls s)} |] ==>
              A |-e {P} {C}e1..m(e2) {S}"
isabelle