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/Library/Array.thy
changeset 28145 af3923ed4786
parent 27695 033732c90ebd
child 28562 4e74209f113e 
--- a/src/HOL/Library/Array.thy	Fri Sep 05 11:50:35 2008 +0200
+++ b/src/HOL/Library/Array.thy	Sat Sep 06 14:02:36 2008 +0200
@@ -57,7 +57,7 @@
   obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')"
     by (cases "Heap_Monad.execute (Array.length a) h")
   then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h"
-    by (auto simp add: upd_def bindM_def run_drop split: sum.split)
+    by (auto simp add: upd_def bindM_def split: sum.split)
 qed
isabelle