author | blanchet |
Tue, 04 Sep 2012 13:02:26 +0200 | |
changeset 49112 | 4de4635d8f93 |
parent 49075 | ed769978dc8d |
child 49123 | 263b0e330d8b |
permissions | -rw-r--r-- |
(* Title: HOL/Codatatype/Codatatype.thy Author: Dmitriy Traytel, TU Muenchen Author: Andrei Popescu, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Copyright 2012 The (co)datatype package. *) header {* The (Co)datatype Package *} theory Codatatype imports BNF_Wrap BNF_LFP BNF_GFP keywords "data" :: thy_decl and "codata" :: thy_decl uses "Tools/bnf_fp_sugar.ML" begin end