| changeset 53305 | 29c267cb9314 |
| parent 53304 | cfef783090eb |
| child 53306 | 45f13517693a |
| 53304:cfef783090eb | 53305:29c267cb9314 |
|---|---|
1 (* Title: HOL/BNF/BNF_LFP_Compat.thy |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2013 |
|
4 |
|
5 Compatibility layer with the old datatype package. |
|
6 *) |
|
7 |
|
8 header {* Compatibility Layer with the Old Datatype Package *} |
|
9 |
|
10 theory BNF_LFP_Compat |
|
11 imports BNF_FP_N2M |
|
12 keywords |
|
13 "datatype_compat" :: thy_goal |
|
14 begin |
|
15 |
|
16 ML_file "Tools/bnf_lfp_compat.ML" |
|
17 |
|
18 end |