Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned equation
authorhaftmann
Wed, 18 Jul 2018 20:51:21 +0200
changeset 68658 16cc1161ad7f
parent 68657 65ad2bfc19d2
child 68659 db0c70767d86
tuned equation
src/HOL/Library/IArray.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:20 2018 +0200
+++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:21 2018 +0200
@@ -52,7 +52,7 @@
 subsection \<open>Generic code equations\<close>
 
 lemma [code]:
-  "size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
+  "size (as :: 'a iarray) = Suc (IArray.length as)"
   by (cases as) simp
 
 lemma [code]:
isabelle