src/HOL/Library/BNF_Axiomatization.thy
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