# 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 \<Rightarrow> nat" where
 [simp]: "length as = List.length (IArray.list_of as)"
 
-qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
-"all p (IArray as) = (\<forall>a \<in> set as. p a)"
+qualified primrec all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+"all p (IArray as) \<longleftrightarrow> (\<forall>a \<in> set as. p a)"
 
-qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
-"exists p (IArray as) = (\<exists>a \<in> set as. p a)"
+qualified primrec exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
+"exists p (IArray as) \<longleftrightarrow> (\<exists>a \<in> set as. p a)"
 
 lemma list_of_code [code]:
 "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"