author | nipkow |
Sun, 05 Jan 2003 21:03:14 +0100 | |
changeset 13771 | 6cd59cc885a1 |
parent 13328 | 703de709a64b |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
12175 | 1 |
(* Title: ZF/Datatype.thy |
2870
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 |
*) |
516 | 7 |
|
13328 | 8 |
header{*Datatype and CoDatatype Definitions*} |
9 |
||
12175 | 10 |
theory Datatype = Inductive + Univ + QUniv |
12183 | 11 |
files |
12 |
"Tools/datatype_package.ML" |
|
13 |
"Tools/numeral_syntax.ML": (*belongs to theory Bin*) |
|
12175 | 14 |
|
15 |
end |