author | haftmann |
Sat, 05 Jul 2014 11:01:53 +0200 | |
changeset 57514 | bdc2c6b40bf2 |
parent 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 |
46753 | 13 |