src/ZF/Main.thy
author wenzelm
Mon, 22 Mar 2010 19:23:03 +0100
changeset 35894 ab6dc4d86ea1
parent 35762 af3ff2ba4c54
permissions -rw-r--r--
added Specification.axiom convenience;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 24893
diff changeset
     1
theory Main 
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 24893
diff changeset
     2
imports Main_ZF
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 24893
diff changeset
     3
begin
12620
4e6626725e21 Some new theorems for ordinals
paulson
parents: 12552
diff changeset
     4
12426
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
     5
end