# HG changeset patch
# User wenzelm
# Date 1433673786 -7200
# Node ID 68eb60fd22a673258267247702176e3f2d94e865
# Parent  b62eaac5c1afc0be9dcedb449296b06e3ecb141c
tuned whitespace;

diff -r b62eaac5c1af -r 68eb60fd22a6 src/HOL/Library/RBT_Mapping.thy
--- 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]: