src/HOL/Old_Number_Theory/BijectionRel.thy
changeset 38159 e9b4835a54ee
parent 32479 521cc9bf2958
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Old_Number_Theory/BijectionRel.thy	Thu Aug 05 23:43:43 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/BijectionRel.thy	Fri Aug 06 12:37:00 2010 +0200
     1.3 @@ -1,10 +1,13 @@
     1.4 -(*  Author:     Thomas M. Rasmussen
     1.5 +(*  Title:      HOL/Old_Number_Theory/BijectionRel.thy
     1.6 +    Author:     Thomas M. Rasmussen
     1.7      Copyright   2000  University of Cambridge
     1.8  *)
     1.9  
    1.10  header {* Bijections between sets *}
    1.11  
    1.12 -theory BijectionRel imports Main begin
    1.13 +theory BijectionRel
    1.14 +imports Main
    1.15 +begin
    1.16  
    1.17  text {*
    1.18    Inductive definitions of bijections between two different sets and