author | blanchet |
Wed, 31 Aug 2011 08:49:10 +0200 | |
changeset 44621 | 9eee93ead24e |
parent 35422 | e74b6f3b950c |
child 46753 | 40e2ada74ce8 |
permissions | -rw-r--r-- |
19203 | 1 |
(* Title: HOL/ZF/MainZF.thy |
2 |
Author: Steven Obua |
|
3 |
||
4 |
Starting point for using HOLZF. |
|
5 |
See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan |
|
6 |
*) |
|
7 |
||
8 |
theory MainZF |
|
9 |
imports Zet LProd |
|
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 | 12 |
end |