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/Bali/DefiniteAssignmentCorrect.thy
changeset 61424 c3658c18b7bc
parent 58887 38db8ddc0f57
child 62042 6c6ccf573479 
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -3962,7 +3962,7 @@
         moreover
         from upd normal_s2
         have "{vn} \<subseteq> dom (locals (store (assign upd v s2)))"
-          by (auto simp add: assign_def Let_def lvar_def upd split: split_split)
+          by (auto simp add: assign_def Let_def lvar_def upd split: prod.split)
         ultimately
         show "nrm A \<subseteq> \<dots>"
           by (rule Un_least [elim_format]) (simp add: nrm_A)
isabelle