src/HOL/Algebra/Bij.thy

--- a/src/HOL/Algebra/Bij.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/HOL/Algebra/Bij.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -10,7 +10,7 @@
 
 definition
   Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
-    \<comment>\<open>Only extensional functions, since otherwise we get too many.\<close>
+    \<comment> \<open>Only extensional functions, since otherwise we get too many.\<close>
    where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
 
 definition