--- a/src/HOL/Fun.thy Tue Aug 02 21:04:52 2016 +0200
+++ b/src/HOL/Fun.thy Tue Aug 02 21:05:34 2016 +0200
@@ -410,8 +410,8 @@
by (auto simp: bij_betw_def)
qed
-lemma bij_betw_cong: "(\<And> a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
- unfolding bij_betw_def inj_on_def by force
+lemma bij_betw_cong: "(\<And>a. a \<in> A \<Longrightarrow> f a = g a) \<Longrightarrow> bij_betw f A A' = bij_betw g A A'"
+ unfolding bij_betw_def inj_on_def by force (* slow *)
lemma bij_betw_id[intro, simp]: "bij_betw id A A"
unfolding bij_betw_def id_def by auto