# HG changeset patch
# User haftmann
# Date 1233997023 -3600
# Node ID 2bc09b164f2beeff43d977407ca359bcbea2f40f
# Parent  c82b3e8a4dafe2a2d5c19f5639f5908fd1bd5cab
added bulkload

diff -r c82b3e8a4daf -r 2bc09b164f2b src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Sat Feb 07 08:37:43 2009 +0100
+++ b/src/HOL/Library/Mapping.thy	Sat Feb 07 09:57:03 2009 +0100
@@ -127,14 +127,6 @@
   "size (tabulate ks f) = length (remdups ks)"
   by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric])
 
-lemma zip_map_fst_snd: (*FIXME move*)
-  "zip (map fst zs) (map snd zs) = zs"
-  by (induct zs) simp_all
-
-lemma zip_eq_conv: (*FIXME move*)
-  "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
-  by (auto simp add: zip_map_fst_snd)
-
 lemma bulkload_tabulate: (*FIXME Isar proof*)
   "bulkload xs = tabulate [0..<length xs] (nth xs)"
   unfolding bulkload_def tabulate_def apply simp