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)