src/HOL/Algebra/Bij.thy
 changeset 61382 efac889fccbc parent 35849 b5522b51cb1e child 63167 0909deb8059b
```     1.1 --- a/src/HOL/Algebra/Bij.thy	Sat Oct 10 16:21:34 2015 +0200
1.2 +++ b/src/HOL/Algebra/Bij.thy	Sat Oct 10 16:26:23 2015 +0200
1.3 @@ -6,11 +6,11 @@
1.4  imports Group
1.5  begin
1.6
1.7 -section {* Bijections of a Set, Permutation and Automorphism Groups *}
1.8 +section \<open>Bijections of a Set, Permutation and Automorphism Groups\<close>
1.9
1.10  definition
1.11    Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
1.12 -    --{*Only extensional functions, since otherwise we get too many.*}
1.13 +    --\<open>Only extensional functions, since otherwise we get too many.\<close>
1.14     where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
1.15
1.16  definition
1.17 @@ -30,7 +30,7 @@
1.18    by (auto simp add: Bij_def bij_betw_imp_funcset)
1.19
1.20
1.21 -subsection {*Bijections Form a Group *}
1.22 +subsection \<open>Bijections Form a Group\<close>
1.23
1.24  lemma restrict_inv_into_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_into S f) x) \<in> Bij S"
1.25    by (simp add: Bij_def bij_betw_inv_into)
1.26 @@ -57,7 +57,7 @@
1.27  done
1.28
1.29
1.30 -subsection{*Automorphisms Form a Group*}
1.31 +subsection\<open>Automorphisms Form a Group\<close>
1.32
1.33  lemma Bij_inv_into_mem: "\<lbrakk> f \<in> Bij S;  x \<in> S\<rbrakk> \<Longrightarrow> inv_into S f x \<in> S"
1.34  by (simp add: Bij_def bij_betw_def inv_into_into)
```