src/HOL/ZF/MainZF.thy
author bulwahn
Mon, 22 Mar 2010 08:30:13 +0100
changeset 35877 295e1af6c8dc
parent 35422 e74b6f3b950c
child 46753 40e2ada74ce8
permissions -rw-r--r--
generalized split transformation in the function flattening
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