author | lcp |
Thu, 06 Apr 1995 12:08:43 +0200 | |
changeset 1014 | 8bec0698d58c |
parent 805 | 96f51689cdeb |
child 2870 | 6d6fd10a9fdc |
permissions | -rw-r--r-- |
578
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
1 |
(*Dummy theory to document dependencies *) |
efc648d29dd0
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
lcp
parents:
diff
changeset
|
2 |
|
805 | 3 |
Inductive = Fixedpt + Sum + QPair + "indrule" |