isabelle: src/HOL/Library/BNF_Axiomatization.thy@123e6dcd3852 (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
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 59794 diff changeset	8	section \<open>Axiomatic Declaration of Bounded Natural Functors\<close>
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
62691 9bfcbab7cd99 put all 'bnf_.ML' files together, irrespective of bootstrapping/dependency constraints blanchet* parents: 60500 diff changeset	16	ML_file "../Tools/BNF/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	wenzelm
	Fri, 14 Oct 2016 21:35:02 +0200
changeset 64215	123e6dcd3852
parent 62691	9bfcbab7cd99
child 69605	a96320074298
permissions	-rw-r--r--