# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1518775397 -3600
# Node ID 3107dcea3493f5d6f0ca489ec939386c4f00dc2e
# Parent  967213048e55e0f9c69ce33dec59e3ce1b377f0f
features and caveats of datatype_record

diff -r 967213048e55 -r 3107dcea3493 src/HOL/Library/Datatype_Records.thy
--- 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"                    ("_")