--- 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"