--- a/src/HOL/Library/Datatype_Records.thy Thu Feb 15 14:36:46 2018 +0100
+++ b/src/HOL/Library/Datatype_Records.thy Fri Feb 16 11:03:17 2018 +0100
@@ -1,3 +1,7 @@
+(* Title: HOL/Library/Datatype_Records.thy
+ Author: Lars Hupel
+*)
+
section \<open>Records based on BNF/datatype machinery\<close>
theory Datatype_Records
@@ -5,6 +9,23 @@
keywords "datatype_record" :: thy_decl
begin
+text \<open>
+ This theory provides an alternative, stripped-down implementation of records based on the
+ machinery of the @{command datatype} package.
+
+ It supports:
+ \<^item> similar declaration syntax as records
+ \<^item> record creation and update syntax (using \<open>\<lparr> ... \<rparr>\<close> brackets)
+ \<^item> regular datatype features (e.g. dead type variables etc.)
+ \<^item> ``after-the-fact'' registration of single-free-constructor types as records
+\<close>
+
+text \<open>
+ Caveats:
+ \<^item> there is no compatibility layer; importing this theory will disrupt existing syntax
+ \<^item> extensible records are not supported
+\<close>
+
no_syntax
"_constify" :: "id => ident" ("_")
"_constify" :: "longid => ident" ("_")