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