src/ZF/Main.thy
author haftmann
Sat, 28 Apr 2012 09:55:01 +0200
changeset 47819 d402ac2288b8
parent 35762 af3ff2ba4c54
permissions -rw-r--r--
rhs of abstract code equations are not subject to preprocessing: inline code abbrevs explicitly
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