| author | bulwahn |
| Sat, 20 Oct 2012 09:09:34 +0200 | |
| changeset 49945 | fb696ff1f086 |
| parent 49510 | ba50d204095e |
| child 51446 | a6ebb12cc003 |
| permissions | -rw-r--r-- |
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49309
diff
changeset
|
1 |
(* Title: HOL/BNF/BNF.thy |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
| 49017 | 3 |
Author: Andrei Popescu, TU Muenchen |
4 |
Author: Jasmin Blanchette, TU Muenchen |
|
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
Copyright 2012 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
|
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49309
diff
changeset
|
7 |
Bounded natural functors for (co)datatypes. |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
*) |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49309
diff
changeset
|
10 |
header {* Bounded Natural Functors for (Co)datatypes *}
|
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
|
|
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49309
diff
changeset
|
12 |
theory BNF |
|
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49308
diff
changeset
|
13 |
imports More_BNFs |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
begin |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
end |