src/ZF/Main.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 35762 af3ff2ba4c54
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
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