--- a/src/HOL/Library/RBT_Mapping.thy Sat Jun 06 13:38:24 2015 +0200
+++ b/src/HOL/Library/RBT_Mapping.thy Sun Jun 07 12:43:06 2015 +0200
@@ -66,13 +66,15 @@
context
notes RBT.bulkload.transfer[transfer_rule del]
begin
- lemma tabulate_Mapping [code]:
- "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\<lambda>k. (k, f k)) ks))"
- by transfer (simp add: map_of_map_restrict)
-
- lemma bulkload_Mapping [code]:
- "Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
- by transfer (simp add: map_of_map_restrict fun_eq_iff)
+
+lemma tabulate_Mapping [code]:
+ "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\<lambda>k. (k, f k)) ks))"
+by transfer (simp add: map_of_map_restrict)
+
+lemma bulkload_Mapping [code]:
+ "Mapping.bulkload vs = Mapping (RBT.bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
+by transfer (simp add: map_of_map_restrict fun_eq_iff)
+
end
lemma equal_Mapping [code]: