changeset 56942 | 5fff4dc31d34 |
parent 55076 | 1e73e090a514 |
child 58881 | b9556a055632 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/BNF_Axiomatization.thy Tue May 13 09:21:22 2014 +0200 @@ -0,0 +1,18 @@ +(* Title: HOL/Library/BNF_Axiomatization.thy + Author: Dmitriy Traytel, TU Muenchen + Copyright 2013 + +Axiomatic declaration of bounded natural functors. +*) + +header {* Axiomatic declaration of Bounded Natural Functors *} + +theory BNF_Axiomatization +imports Main +keywords + "bnf_axiomatization" :: thy_decl +begin + +ML_file "bnf_axiomatization.ML" + +end