author | wenzelm |
Sat, 29 Feb 2020 16:30:30 +0100 | |
changeset 71495 | 633a8d52fef2 |
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 |