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 69097 e65ab21821bf
parent 69085 9999d7823b8f 
--- a/src/HOL/MicroJava/Comp/Index.thy	Sat Sep 29 16:30:44 2018 -0400
+++ b/src/HOL/MicroJava/Comp/Index.thy	Sun Sep 30 18:19:28 2018 -0400
@@ -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