slightly more uniform style
authorhaftmann
Wed Jul 18 20:51:19 2018 +0200 (4 weeks ago)
changeset 68656297ca38c7da5
parent 68655 90652333fae2
child 68657 65ad2bfc19d2
slightly more uniform style
src/HOL/Library/IArray.thy
     1.1 --- a/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:17 2018 +0200
     1.2 +++ b/src/HOL/Library/IArray.thy	Wed Jul 18 20:51:19 2018 +0200
     1.3 @@ -30,11 +30,11 @@
     1.4  qualified definition length :: "'a iarray \<Rightarrow> nat" where
     1.5  [simp]: "length as = List.length (IArray.list_of as)"
     1.6  
     1.7 -qualified fun all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
     1.8 -"all p (IArray as) = (\<forall>a \<in> set as. p a)"
     1.9 +qualified primrec all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    1.10 +"all p (IArray as) \<longleftrightarrow> (\<forall>a \<in> set as. p a)"
    1.11  
    1.12 -qualified fun exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    1.13 -"exists p (IArray as) = (\<exists>a \<in> set as. p a)"
    1.14 +qualified primrec exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a iarray \<Rightarrow> bool" where
    1.15 +"exists p (IArray as) \<longleftrightarrow> (\<exists>a \<in> set as. p a)"
    1.16  
    1.17  lemma list_of_code [code]:
    1.18  "IArray.list_of as = map (\<lambda>n. as !! n) [0 ..< IArray.length as]"