author | wenzelm |
Tue, 08 Aug 2000 16:57:44 +0200 | |
changeset 9558 | 8d5221bf765b |
parent 6070 | 032babd0120b |
child 12175 | 5cf58a1799a7 |
permissions | -rw-r--r-- |
2870
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset
|
1 |
(* Title: ZF/Datatype |
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset
|
2 |
ID: $Id$ |
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset
|
4 |
Copyright 1997 University of Cambridge |
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset
|
5 |
|
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset
|
6 |
Dummy theory: brings in all ancestors needed for (Co)Datatype Declarations |
124 | 7 |
|
2870
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset
|
8 |
"Datatype" must be capital to avoid conflicts with ML's "datatype" |
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
809
diff
changeset
|
9 |
*) |
516 | 10 |
|
6070 | 11 |
Datatype = Inductive + Univ + QUniv |