author | blanchet |
Tue, 11 Sep 2012 17:14:49 +0200 | |
changeset 49283 | 97809ae5f7bb |
parent 49123 | 263b0e330d8b |
child 49286 | dde4967c9233 |
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_LFP BNF_GFP BNF_Wrap keywords "data" :: thy_decl and "codata" :: thy_decl uses "Tools/bnf_fp_sugar_tactics.ML" "Tools/bnf_fp_sugar.ML" begin end