src/ZF/Main.thy
author hoelzl
Fri, 22 Apr 2016 15:18:46 +0200
changeset 63052 c968bce3921e
parent 35762 af3ff2ba4c54
permissions -rw-r--r--
Linear_Algebra: generalize linear_independent_extend to all real vector spaces
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