| author | Andreas Lochbihler |
| Wed, 11 Nov 2015 10:13:40 +0100 | |
| changeset 61633 | 64e6d712af16 |
| parent 60500 | 903bb1495239 |
| child 62691 | 9bfcbab7cd99 |
| permissions | -rw-r--r-- |
(* Title: HOL/Library/BNF_Axiomatization.thy Author: Dmitriy Traytel, TU Muenchen Copyright 2013 Axiomatic declaration of bounded natural functors. *) section \<open>Axiomatic Declaration of Bounded Natural Functors\<close> theory BNF_Axiomatization imports Main keywords "bnf_axiomatization" :: thy_decl begin ML_file "bnf_axiomatization.ML" end