| author | Andreas Lochbihler |
| Wed, 14 Jan 2015 15:22:50 +0100 | |
| changeset 59359 | 07b9893cd8a7 |
| parent 58881 | b9556a055632 |
| child 59794 | 39442248a027 |
| permissions | -rw-r--r-- |
(* Title: HOL/Library/BNF_Axiomatization.thy Author: Dmitriy Traytel, TU Muenchen Copyright 2013 Axiomatic declaration of bounded natural functors. *) section {* Axiomatic declaration of Bounded Natural Functors *} theory BNF_Axiomatization imports Main keywords "bnf_axiomatization" :: thy_decl begin ML_file "bnf_axiomatization.ML" end