tuned header
authorhaftmann
Tue, 10 Nov 2009 16:11:46 +0100
changeset 33596 27c5023ee818
parent 33595 7264824baf66
child 33597 702c2a771be6
tuned header
src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Tue Nov 10 16:11:43 2009 +0100
+++ b/src/HOL/ex/Records.thy	Tue Nov 10 16:11:46 2009 +0100
@@ -5,7 +5,9 @@
 
 header {* Using extensible records in HOL -- points and coloured points *}
 
-theory Records imports Main begin
+theory Records
+imports Main Record
+begin
 
 subsection {* Points *}