src/ZF/Main.thy
author huffman
Fri, 27 Jul 2012 17:57:31 +0200
changeset 48559 686cc7c47589
parent 35762 af3ff2ba4c54
permissions -rw-r--r--
give Nat_Arith simprocs proper name bindings by using simproc_setup
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