src/ZF/Main.thy
author wenzelm
Thu, 17 Dec 2009 15:09:07 +0100
changeset 34096 e438a5875c16
parent 26057 f5d5c4922cdf
child 35762 af3ff2ba4c54
permissions -rw-r--r--
simplified message format: chunks with explicit size in bytes; robust message header via YXML.binary_text; standard_message: refer to thread position only; discontinued obsolete "-" output stream; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26057
f5d5c4922cdf added Id;
wenzelm
parents: 26056
diff changeset
     1
(* $Id$ *)
f5d5c4922cdf added Id;
wenzelm
parents: 26056
diff changeset
     2
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 24893
diff changeset
     3
theory Main 
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 24893
diff changeset
     4
imports Main_ZF
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 24893
diff changeset
     5
begin
12620
4e6626725e21 Some new theorems for ordinals
paulson
parents: 12552
diff changeset
     6
12426
9032bdbc2125 new-style theory;
wenzelm
parents: 9578
diff changeset
     7
end