src/ZF/Main_ZFC.thy
author huffman
Mon, 08 Jun 2009 11:48:19 -0700
changeset 31527 a971fd7d8e45
parent 26057 f5d5c4922cdf
child 35762 af3ff2ba4c54
permissions -rw-r--r--
generalize lemmas eventually_within_interior, lim_within_interior
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26057
f5d5c4922cdf added Id;
wenzelm
parents: 26056
diff changeset
     1
(* $Id$ *)
f5d5c4922cdf added Id;
wenzelm
parents: 26056
diff changeset
     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