src/HOL/Algebra/Bij.thy
changeset 20318 0e0ea63fe768
parent 16417 9bc16273c2d4
child 27717 21bbd410ba04
     1.1 --- a/src/HOL/Algebra/Bij.thy	Thu Aug 03 14:53:57 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Bij.thy	Thu Aug 03 14:57:26 2006 +0200
     1.3 @@ -3,9 +3,10 @@
     1.4      Author:     Florian Kammueller, with new proofs by L C Paulson
     1.5  *)
     1.6  
     1.7 -header {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
     1.8 +theory Bij imports Group begin
     1.9  
    1.10 -theory Bij imports Group begin
    1.11 +
    1.12 +section {* Bijections of a Set, Permutation Groups and Automorphism Groups *}
    1.13  
    1.14  constdefs
    1.15    Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"