| author | wenzelm | 
| Tue, 08 Feb 2011 19:57:11 +0100 | |
| changeset 41731 | 2fb760843e17 | 
| 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  |