author | haftmann |
Tue, 10 Nov 2009 16:11:46 +0100 | |
changeset 33596 | 27c5023ee818 |
parent 33595 | 7264824baf66 |
child 33597 | 702c2a771be6 |
--- 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 *}