# HG changeset patch
# User haftmann
# Date 1233997389 -3600
# Node ID 5dc920623bb140b1ecd4342fb0549e49e2ad4f9e
# Parent  edac6cd013108385a7f8470187b4d05369a5a1c3
Isar proof

diff -r edac6cd01310 -r 5dc920623bb1 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Sat Feb 07 09:58:24 2009 +0100
+++ b/src/HOL/Library/Mapping.thy	Sat Feb 07 10:03:09 2009 +0100
@@ -127,16 +127,9 @@
   "size (tabulate ks f) = length (remdups ks)"
   by (simp add: size_def keys_tabulate distinct_card [of "remdups ks", symmetric])
 
-lemma bulkload_tabulate: (*FIXME Isar proof*)
+lemma bulkload_tabulate:
   "bulkload xs = tabulate [0..<length xs] (nth xs)"
-  unfolding bulkload_def tabulate_def apply simp
-  apply (rule sym)
-  apply (rule ext) apply auto
-  apply (subst map_of_eq_Some_iff)
-  apply (simp add: map_compose [symmetric] comp_def)
-  apply (simp add: image_def)
-  apply (subst map_of_eq_None_iff)
-  apply (simp add: image_def)
-  done
+  by (rule sym)
+    (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def)
 
 end
\ No newline at end of file