--- 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
-