# HG changeset patch # User haftmann # Date 1257865906 -3600 # Node ID 27c5023ee8182565170984c3ae0ab7ae0276b90b # Parent 7264824baf660acec75c30ea9e3f67c866b32369 tuned header diff -r 7264824baf66 -r 27c5023ee818 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 *}