isabelle: src/HOL/ZF/MainZF.thy@85bc9b7c4d18 (annotated)

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