| author | oheimb |
| Wed, 12 Nov 1997 18:58:50 +0100 | |
| changeset 4223 | f60e3d2c81d3 |
| parent 2870 | 6d6fd10a9fdc |
| child 6053 | 8a1059aa01f0 |
| 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 |
|
|
2870
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
805
diff
changeset
|
3 |
Inductive = Fixedpt + Sum + QPair + "indrule" + |
|
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
805
diff
changeset
|
4 |
|
|
6d6fd10a9fdc
Now a non-trivial theory so that require_thy can find it
paulson
parents:
805
diff
changeset
|
5 |
end |