author | blanchet |
Tue, 11 Sep 2012 18:39:47 +0200 | |
changeset 49286 | dde4967c9233 |
parent 49284 | 5f39b7940b49 |
child 49309 | f20b24214ac2 |
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_Util keywords "print_bnfs" :: diag and "bnf_def" :: thy_goal uses "Tools/bnf_def_tactics.ML" "Tools/bnf_def.ML" begin end