| author | blanchet | 
| Thu, 26 Jun 2014 13:36:06 +0200 | |
| changeset 57373 | e9d47cd3239b | 
| parent 56942 | 5fff4dc31d34 | 
| child 58881 | b9556a055632 | 
| permissions | -rw-r--r-- | 
(* 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