author | lcp |
Fri, 09 Sep 1994 11:57:49 +0200 | |
changeset 596 | cffb278ec83e |
parent 578 | efc648d29dd0 |
child 809 | 1daa0269eb5d |
permissions | -rw-r--r-- |
124 | 1 |
(*Dummy theory to document dependencies *) |
2 |
||
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
516
diff
changeset
|
3 |
Datatype = "constructor" + "Inductive" + Univ + QUniv |
516 | 4 |
|
5 |
(*Datatype must be capital to avoid conflicts with ML's "datatype" *) |