src/HOL/ZF/MainZF.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46753 40e2ada74ce8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
46753
40e2ada74ce8 tuned whitespace
haftmann
parents: 35422
diff changeset
    13