changeset 33640 | 0d82107dc07a |
parent 31459 | ae39b7b2a68a |
child 35157 | 73cd6f78c86d |
--- a/src/HOL/Library/Mapping.thy Thu Nov 12 17:21:48 2009 +0100 +++ b/src/HOL/Library/Mapping.thy Thu Nov 12 17:21:51 2009 +0100 @@ -128,7 +128,7 @@ lemma bulkload_tabulate: "bulkload xs = tabulate [0..<length xs] (nth xs)" by (rule sym) - (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff map_compose [symmetric] comp_def) + (auto simp add: bulkload_def tabulate_def expand_fun_eq map_of_eq_None_iff comp_def) subsection {* Some technical code lemmas *}