| author | blanchet |
| Tue, 28 Aug 2012 17:19:59 +0200 | |
| changeset 48979 | b62d14275b89 |
| parent 48975 | 7f79f94a432c |
| child 49017 | 66fc7fc2d49b |
| permissions | -rw-r--r-- |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Codatatype/Codatatype.thy |
|
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 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
The (co)datatype package. |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
header {* The (Co)datatype Package *}
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
theory Codatatype |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
imports BNF_LFP BNF_GFP |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
begin |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
|
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
end |