equal
deleted
inserted
replaced
1 (* Title: HOL/Codatatype/Codatatype.thy |
1 (* Title: HOL/Codatatype/Codatatype.thy |
2 Author: Dmitriy Traytel, TU Muenchen |
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Author: Jasmin Blanchette, TU Muenchen |
3 Copyright 2012 |
5 Copyright 2012 |
4 |
6 |
5 The (co)datatype package. |
7 The (co)datatype package. |
6 *) |
8 *) |
7 |
9 |
8 header {* The (Co)datatype Package *} |
10 header {* The (Co)datatype Package *} |
9 |
11 |
10 theory Codatatype |
12 theory Codatatype |
11 imports BNF_LFP BNF_GFP |
13 imports BNF_LFP BNF_GFP |
|
14 keywords |
|
15 "bnf_sugar" :: thy_goal |
|
16 uses |
|
17 "Tools/bnf_sugar.ML" |
12 begin |
18 begin |
13 |
19 |
14 end |
20 end |