isabelle: src/HOL/Library/BNF_Axiomatization.thy@7f2b60cb5190 (annotated)

56942 5fff4dc31d34 bnf_decl -> bnf_axiomatization traytel parents: 55076 diff changeset	1	(* Title: HOL/Library/BNF_Axiomatization.thy
54601 91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	2	Author: Dmitriy Traytel, TU Muenchen
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	3	Copyright 2013
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	4
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	5	Axiomatic declaration of bounded natural functors.
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	6	*)
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	7
58881 b9556a055632 modernized header; wenzelm parents: 56942 diff changeset	8	section {* Axiomatic declaration of Bounded Natural Functors *}
54601 91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	9
56942 5fff4dc31d34 bnf_decl -> bnf_axiomatization traytel parents: 55076 diff changeset	10	theory BNF_Axiomatization
55075 b3d0a02a756d dissolved BNF session blanchet parents: 54601 diff changeset	11	imports Main
54601 91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	12	keywords
56942 5fff4dc31d34 bnf_decl -> bnf_axiomatization traytel parents: 55076 diff changeset	13	"bnf_axiomatization" :: thy_decl
54601 91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	14	begin
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	15
56942 5fff4dc31d34 bnf_decl -> bnf_axiomatization traytel parents: 55076 diff changeset	16	ML_file "bnf_axiomatization.ML"
54601 91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	17
91a1e4aa7c80 command for axiomatic declaration of bnfs---allow theoreticians to fix an arbitrary type with functorial structure and work abstractly on it traytel parents: diff changeset	18	end

author	haftmann
	Sat, 14 Feb 2015 10:24:15 +0100
changeset 59537	7f2b60cb5190
parent 58881	b9556a055632
child 59794	39442248a027
permissions	-rw-r--r--