equal
deleted
inserted
replaced
1 (* Title: HOL/Algebra/Bij.thy |
1 (* Title: HOL/Algebra/Bij.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Kammueller, with new proofs by L C Paulson |
3 Author: Florian Kammueller, with new proofs by L C Paulson |
4 *) |
4 *) |
5 |
5 |
6 header {* Bijections of a Set, Permutation Groups, Automorphism Groups *} |
6 theory Bij imports Group begin |
7 |
7 |
8 theory Bij imports Group begin |
8 |
|
9 section {* Bijections of a Set, Permutation Groups and Automorphism Groups *} |
9 |
10 |
10 constdefs |
11 constdefs |
11 Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" |
12 Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" |
12 --{*Only extensional functions, since otherwise we get too many.*} |
13 --{*Only extensional functions, since otherwise we get too many.*} |
13 "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}" |
14 "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}" |