author | blanchet |
Tue, 11 Sep 2012 17:14:49 +0200 | |
changeset 49283 | 97809ae5f7bb |
parent 49074 | d8af889dcbe3 |
child 49308 | 6190b701e4f4 |
permissions | -rw-r--r-- |
(* Title: HOL/Codatatype/BNF_GFP.thy Author: Dmitriy Traytel, TU Muenchen Copyright 2012 Greatest fixed point operation on bounded natural functors. *) header {* Greatest Fixed Point Operation on Bounded Natural Functors *} theory BNF_GFP imports BNF_Comp keywords "codata_raw" :: thy_decl uses "Tools/bnf_gfp_util.ML" "Tools/bnf_gfp_tactics.ML" "Tools/bnf_gfp.ML" begin end