fixed proof
authorhaftmann
Wed Apr 23 19:36:18 2008 +0200 (2008-04-23)
changeset 26743f4cf7d36c63a
parent 26742 5a86bc79431c
child 26744 7b9439678304
fixed proof
src/HOL/Library/Array.thy
     1.1 --- a/src/HOL/Library/Array.thy	Wed Apr 23 15:04:14 2008 +0200
     1.2 +++ b/src/HOL/Library/Array.thy	Wed Apr 23 19:36:18 2008 +0200
     1.3 @@ -164,8 +164,7 @@
     1.4  hide (open) const upd'
     1.5  lemma [code func]:
     1.6    "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
     1.7 -  apply (simp add: upd'_def monad_simp)
     1.8 -oops
     1.9 +  by (simp add: upd'_def monad_simp upd_return)
    1.10  
    1.11  
    1.12  subsubsection {* SML *}