# HG changeset patch # User haftmann # Date 1531939879 -7200 # Node ID 297ca38c7da5977e0307e64eb10776222f6a3639 # Parent 90652333fae21244d2f6728661776091ffbbb41c slightly more uniform style diff -r 90652333fae2 -r 297ca38c7da5 src/HOL/Library/IArray.thy --- a/src/HOL/Library/IArray.thy Wed Jul 18 20:51:17 2018 +0200 +++ b/src/HOL/Library/IArray.thy Wed Jul 18 20:51:19 2018 +0200 @@ -30,11 +30,11 @@ qualified definition length :: "'a iarray \ nat" where [simp]: "length as = List.length (IArray.list_of as)" -qualified fun all :: "('a \ bool) \ 'a iarray \ bool" where -"all p (IArray as) = (\a \ set as. p a)" +qualified primrec all :: "('a \ bool) \ 'a iarray \ bool" where +"all p (IArray as) \ (\a \ set as. p a)" -qualified fun exists :: "('a \ bool) \ 'a iarray \ bool" where -"exists p (IArray as) = (\a \ set as. p a)" +qualified primrec exists :: "('a \ bool) \ 'a iarray \ bool" where +"exists p (IArray as) \ (\a \ set as. p a)" lemma list_of_code [code]: "IArray.list_of as = map (\n. as !! n) [0 ..< IArray.length as]"