| author | huffman |
| Mon, 08 Mar 2010 14:42:40 -0800 | |
| changeset 35663 | ada7bc39c6b1 |
| 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 |