reverted half-baken 7d1127ac2251
authorhaftmann
Sat Nov 14 08:45:51 2015 +0100 (2015-11-14)
changeset 616689a51e4dfc5d9
parent 61667 4b53042d7a40
child 61669 27ca6147e3b3
reverted half-baken 7d1127ac2251
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sat Nov 14 08:45:51 2015 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Nov 14 08:45:51 2015 +0100
     1.3 @@ -6408,15 +6408,6 @@
     1.4    "map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
     1.5    by (simp add: map_filter_def)
     1.6  
     1.7 -definition map_range :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list"
     1.8 -where
     1.9 -  [code_abbrev]: "map_range f n = map f [0..<n]"
    1.10 -
    1.11 -lemma map_range_simps [simp, code]:
    1.12 -  "map_range f 0 = []"
    1.13 -  "map_range f (Suc n) = map_range f n @ [f n]"
    1.14 -  by (simp_all add: map_range_def)
    1.15 -
    1.16  text \<open>Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
    1.17  and similiarly for @{text"\<exists>"}.\<close>
    1.18