tuned whitespace;
authorwenzelm
Sun Jun 07 12:43:06 2015 +0200 (2015-06-07)
changeset 6037368eb60fd22a6
parent 60372 b62eaac5c1af
child 60374 6b858199f240
tuned whitespace;
src/HOL/Library/RBT_Mapping.thy
     1.1 --- a/src/HOL/Library/RBT_Mapping.thy	Sat Jun 06 13:38:24 2015 +0200
     1.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Sun Jun 07 12:43:06 2015 +0200
     1.3 @@ -66,13 +66,15 @@
     1.4  context
     1.5    notes RBT.bulkload.transfer[transfer_rule del]
     1.6  begin
     1.7 -  lemma tabulate_Mapping [code]:
     1.8 -    "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\<lambda>k. (k, f k)) ks))"
     1.9 -  by transfer (simp add: map_of_map_restrict)
    1.10 -  
    1.11 -  lemma bulkload_Mapping [code]:
    1.12 -    "Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
    1.13 -  by transfer (simp add: map_of_map_restrict fun_eq_iff)
    1.14 +
    1.15 +lemma tabulate_Mapping [code]:
    1.16 +  "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\<lambda>k. (k, f k)) ks))"
    1.17 +by transfer (simp add: map_of_map_restrict)
    1.18 +
    1.19 +lemma bulkload_Mapping [code]:
    1.20 +  "Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
    1.21 +by transfer (simp add: map_of_map_restrict fun_eq_iff)
    1.22 +
    1.23  end
    1.24  
    1.25  lemma equal_Mapping [code]: