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/Comp/Index.thy
changeset 69085 9999d7823b8f
parent 63040 eb4ddd18d635 
--- a/src/HOL/MicroJava/Comp/Index.thy	Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy	Sun Sep 30 09:00:11 2018 +0200
@@ -70,7 +70,7 @@
 lemma update_at_index: "
   \<lbrakk> distinct (gjmb_plns (gmb G C S));
   x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow>
-  locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] =
+  (locvars_xstate G C S (Norm (h, l)))[index (gmb G C S) x := val] =
   locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))"
   apply (simp only: locvars_xstate_def locvars_locals_def index_def)
   apply (case_tac "gmb G C S" rule: prod.exhaust, simp)
isabelle