diff -r 143f58bb34f9 -r 0909deb8059b 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 \ ('a \ 'a) set"
- --\Only extensional functions, since otherwise we get too many.\
+ \\Only extensional functions, since otherwise we get too many.\
where "Bij S = extensional S \ {f. bij_betw f S S}"
definition