| author | wenzelm | 
| Sat, 18 Jun 2011 23:51:22 +0200 | |
| changeset 43453 | 3c9696efe6b4 | 
| parent 35762 | af3ff2ba4c54 | 
| permissions | -rw-r--r-- | 
| 12175 | 1  | 
(* Title: ZF/ROOT.ML  | 
| 1461 | 2  | 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory  | 
| 0 | 3  | 
Copyright 1993 University of Cambridge  | 
4  | 
||
| 12175 | 5  | 
Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.  | 
6  | 
This theory is the work of Martin Coen, Philippe Noel and Lawrence  | 
|
7  | 
Paulson.  | 
|
| 0 | 8  | 
*)  | 
9  | 
||
| 26058 | 10  | 
use_thys ["Main", "Main_ZFC"];  | 
| 0 | 11  |