src/HOL/Library/RBT_Mapping.thy
changeset 60373 68eb60fd22a6
parent 58881 b9556a055632
child 60500 903bb1495239
--- 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]: