tuned equation
authorhaftmann
Wed Jul 18 20:51:21 2018 +0200 (5 months ago)
changeset 6865816cc1161ad7f
parent 68657 65ad2bfc19d2
child 68659 db0c70767d86
tuned equation
src/HOL/Library/IArray.thy
     1.1 --- a/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:20 2018 +0200
     1.2 +++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:21 2018 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4  subsection \<open>Generic code equations\<close>
     1.5  
     1.6  lemma [code]:
     1.7 -  "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
     1.8 +  "size (as :: 'a iarray) = Suc (IArray.length as)"
     1.9    by (cases as) simp
    1.10  
    1.11  lemma [code]: