src/HOL/ZF/MainZF.thy
author haftmann
Mon, 01 Mar 2010 13:40:23 +0100
changeset 35416 d8d7d1b785af
parent 19203 778507520684
child 35422 e74b6f3b950c
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
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
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents:
diff changeset
    12
end