| author | bulwahn | 
| Fri, 11 Nov 2011 12:10:49 +0100 | |
| changeset 45461 | 130c90bb80b4 | 
| 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  |