# HG changeset patch
# User wenzelm
# Date 1177598351 -7200
# Node ID 9dfadec17cc41e3d5f6c3229c01d02b7a3696a84
# Parent  0eba117368d92dcf6d2c611ea914bf2c3411db25
added header;

diff -r 0eba117368d9 -r 9dfadec17cc4 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Thu Apr 26 16:39:10 2007 +0200
+++ b/src/HOL/Record.thy	Thu Apr 26 16:39:11 2007 +0200
@@ -3,6 +3,8 @@
     Author:     Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen
 *)
 
+header {* Extensible records with structural subtyping *}
+
 theory Record
 imports Product_Type
 uses ("Tools/record_package.ML")
@@ -27,6 +29,7 @@
 lemma K_record_cong [cong]: "K_record c x = K_record c x"
   by (rule refl)
 
+
 subsection {* Concrete record syntax *}
 
 nonterminals
@@ -64,4 +67,3 @@
 setup RecordPackage.setup
 
 end
-