# HG changeset patch
# User haftmann
# Date 1274448157 -7200
# Node ID a89b47a94b19d80068ce4db8bf4f98b2b0d4d892
# Parent  80dd92673fcad86eb1fa0a4c3da8bf39b1917e41
tuned

diff -r 80dd92673fca -r a89b47a94b19 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri May 21 15:22:37 2010 +0200
+++ b/src/HOL/Library/RBT.thy	Fri May 21 15:22:37 2010 +0200
@@ -222,7 +222,8 @@
   "Mapping.bulkload vs = Mapping (bulkload (List.map (\<lambda>n. (n, vs ! n)) [0..<length vs]))"
   by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
 
-lemma [code, code del]: "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
+lemma [code, code del]:
+  "HOL.eq (x :: (_, _) mapping) y \<longleftrightarrow> x = y" by (fact eq_equals) (*FIXME*)
 
 lemma eq_Mapping [code]:
   "HOL.eq (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"