src/HOL/Algebra/Bij.thy
changeset 67443 3abf6a722518
parent 67091 1393c2340eec
child 68687 2976a4a3b126
     1.1 --- a/src/HOL/Algebra/Bij.thy	Tue Jan 16 09:12:16 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Tue Jan 16 09:30:00 2018 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  definition
     1.6    Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
     1.7 -    \<comment>\<open>Only extensional functions, since otherwise we get too many.\<close>
     1.8 +    \<comment> \<open>Only extensional functions, since otherwise we get too many.\<close>
     1.9     where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
    1.10  
    1.11  definition