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