isabelle: src/HOL/Library/BNF_Decl.thy@2d8222c76020 (annotated)

55075 b3d0a02a756d dissolved BNF session blanchet parents: 54601 diff changeset	1	(* Title: HOL/Library/BNF_Decl.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
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	8	header {* 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	9
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	10	theory BNF_Decl
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
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	13	"bnf_decl" :: thy_decl
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
55076 1e73e090a514 compile blanchet parents: 55075 diff changeset	16	ML_file "bnf_decl.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	nipkow
	Fri, 07 Feb 2014 22:37:43 +0100
changeset 55359	2d8222c76020
parent 55076	1e73e090a514
permissions	-rw-r--r--