isabelle: src/HOL/Library/BNF_Axiomatization.thy@b69fd6e19662 (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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 62691 diff changeset	16	ML_file \<open>../Tools/BNF/bnf_axiomatization.ML\<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	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>
	Fri, 08 Jan 2021 16:07:34 +0000
changeset 73103	b69fd6e19662
parent 69605	a96320074298
permissions	-rw-r--r--