author | blanchet |
Tue, 28 Aug 2012 17:16:00 +0200 | |
changeset 48975 | 7f79f94a432c |
child 49282 | c057e1b39f16 |
permissions | -rw-r--r-- |
(* Title: HOL/Codatatype/BNF_Def.thy Author: Dmitriy Traytel, TU Muenchen Copyright 2012 Definition of bounded natural functors. *) header {* Definition of Bounded Natural Functors *} theory BNF_Def imports BNF_Library keywords "print_bnfs" :: diag and "bnf_def" :: thy_goal uses "Tools/bnf_util.ML" "Tools/bnf_tactics.ML" "Tools/bnf_def.ML" begin end