isabelle: src/HOL/Library/BNF_Axiomatization.thy@9b0825a00b1a (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
59794 39442248a027 tuning blanchet parents: 58881 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	paulson <lp15@cam.ac.uk>
	Tue, 28 Apr 2015 16:23:05 +0100
changeset 60149	9b0825a00b1a
parent 59794	39442248a027
child 60500	903bb1495239
permissions	-rw-r--r--