author | wenzelm |
Sun, 06 Jan 2019 15:04:34 +0100 | |
changeset 69605 | a96320074298 |
parent 62691 | 9bfcbab7cd99 |
permissions | -rw-r--r-- |
56942 | 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 | 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 | 10 |
theory BNF_Axiomatization |
55075 | 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 | 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 | 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 |