| author | haftmann | 
| Tue, 20 Oct 2009 08:10:47 +0200 | |
| changeset 33008 | b0ff69f0a248 | 
| 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: 
16417diff
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 |