| author | blanchet |
| Thu, 16 Jan 2014 16:20:17 +0100 | |
| changeset 55017 | 2df6ad1dbd66 |
| parent 54601 | 91a1e4aa7c80 |
| permissions | -rw-r--r-- |
|
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
|
1 |
(* Title: HOL/BNF/BNF_Decl.thy |
|
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 |
|
|
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
|
10 |
theory BNF_Decl |
|
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
|
11 |
imports BNF_Def |
|
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 |
|
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
|
13 |
"bnf_decl" :: thy_decl |
|
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 |
|
|
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
|
16 |
ML_file "Tools/bnf_decl.ML" |
|
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 |