equal
deleted
inserted
replaced
4 |
4 |
5 section \<open>Records based on BNF/datatype machinery\<close> |
5 section \<open>Records based on BNF/datatype machinery\<close> |
6 |
6 |
7 theory Datatype_Records |
7 theory Datatype_Records |
8 imports Main |
8 imports Main |
9 keywords "datatype_record" :: thy_decl |
9 keywords "datatype_record" :: thy_defn |
10 begin |
10 begin |
11 |
11 |
12 text \<open> |
12 text \<open> |
13 This theory provides an alternative, stripped-down implementation of records based on the |
13 This theory provides an alternative, stripped-down implementation of records based on the |
14 machinery of the @{command datatype} package. |
14 machinery of the @{command datatype} package. |