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/Imperative_HOL/ex/SatChecker.thy
changeset 69085 9999d7823b8f
parent 68028 1f9f973eed2a 
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sun Sep 30 07:46:38 2018 +0200
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Sun Sep 30 09:00:11 2018 +0200
@@ -130,7 +130,7 @@
   assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
   shows "cl \<in> array_ran a h \<or> cl = b"
 proof -
-  have "set (Array.get h a[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
+  have "set ((Array.get h a)[i := Some b]) \<subseteq> insert (Some b) (set (Array.get h a))" by (rule set_update_subset_insert)
   with assms show ?thesis 
     unfolding array_ran_def Array.update_def by fastforce
 qed
@@ -139,7 +139,7 @@
   assumes "cl \<in> array_ran a (Array.update a i None h)"
   shows "cl \<in> array_ran a h"
 proof -
-  have "set (Array.get h a[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
+  have "set ((Array.get h a)[i := None]) \<subseteq> insert None (set (Array.get h a))" by (rule set_update_subset_insert)
   with assms show ?thesis
     unfolding array_ran_def Array.update_def by auto
 qed
isabelle