| author | dixon |
| Sun, 01 Jun 2008 17:45:43 +0200 | |
| changeset 27033 | 6ef5134fc631 |
| parent 26057 | f5d5c4922cdf |
| child 35762 | af3ff2ba4c54 |
| permissions | -rw-r--r-- |
| 26057 | 1 |
(* $Id$ *) |
2 |
||
|
26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
16417
diff
changeset
|
3 |
theory Main_ZFC imports Main_ZF InfDatatype begin |
|
12552
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff
changeset
|
4 |
|
|
d2d2ab3f1f37
separation of the AC part of Main into Main_ZFC, plus a few new lemmas
paulson
parents:
diff
changeset
|
5 |
end |