src/HOL/ZF/MainZF.thy
author wenzelm
Mon, 01 Mar 2010 17:45:19 +0100
changeset 35422 e74b6f3b950c
parent 35416 d8d7d1b785af
child 46753 40e2ada74ce8
permissions -rw-r--r--
tuned final whitespace;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     1
(*  Title:      HOL/ZF/MainZF.thy
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     2
    Author:     Steven Obua
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     3
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     4
    Starting point for using HOLZF.
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     5
    See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     6
*)
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     7
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     8
theory MainZF
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
     9
imports Zet LProd
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    10
begin
35416
d8d7d1b785af replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents: 19203
diff changeset
    11
35422
e74b6f3b950c tuned final whitespace;
wenzelm
parents: 35416
diff changeset
    12
end