author | blanchet |
Mon, 20 Jan 2014 18:24:56 +0100 | |
changeset 55075 | b3d0a02a756d |
parent 54601 | src/HOL/BNF/BNF_Decl.thy@91a1e4aa7c80 |
child 55076 | 1e73e090a514 |
permissions | -rw-r--r-- |
(* Title: HOL/Library/BNF_Decl.thy Author: Dmitriy Traytel, TU Muenchen Copyright 2013 Axiomatic declaration of bounded natural functors. *) header {* Axiomatic declaration of Bounded Natural Functors *} theory BNF_Decl imports Main keywords "bnf_decl" :: thy_decl begin ML_file "Tools/bnf_decl.ML" end