tuned header
authorhaftmann
Tue Nov 10 16:11:46 2009 +0100 (2009-11-10)
changeset 3359627c5023ee818
parent 33595 7264824baf66
child 33597 702c2a771be6
tuned header
src/HOL/ex/Records.thy
     1.1 --- a/src/HOL/ex/Records.thy	Tue Nov 10 16:11:43 2009 +0100
     1.2 +++ b/src/HOL/ex/Records.thy	Tue Nov 10 16:11:46 2009 +0100
     1.3 @@ -5,7 +5,9 @@
     1.4  
     1.5  header {* Using extensible records in HOL -- points and coloured points *}
     1.6  
     1.7 -theory Records imports Main begin
     1.8 +theory Records
     1.9 +imports Main Record
    1.10 +begin
    1.11  
    1.12  subsection {* Points *}
    1.13