src/HOL/Algebra/Bij.thy
changeset 63167 0909deb8059b
parent 61382 efac889fccbc
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Algebra/Bij.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  definition
     1.6    Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
     1.7 -    --\<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