src/ZF/Main.thy
author wenzelm
Tue, 21 Jul 2009 01:03:18 +0200
changeset 32091 30e2ffbba718
parent 26057 f5d5c4922cdf
child 35762 af3ff2ba4c54
permissions -rw-r--r--
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
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