src/HOL/Algebra/Bij.thy

--- a/src/HOL/Algebra/Bij.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/Algebra/Bij.thy	Thu May 26 17:51:22 2016 +0200
@@ -10,7 +10,7 @@
 
 definition
   Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
-    --\<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