author | blanchet |
Thu, 28 Aug 2014 07:30:16 +0200 | |
changeset 58066 | 96e987003a01 |
parent 56942 | 5fff4dc31d34 |
child 58881 | b9556a055632 |
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 |
|
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 |
|
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 |
|
56942 | 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 |