| author | bulwahn | 
| Wed, 19 Oct 2011 08:37:27 +0200 | |
| changeset 45181 | c8eb935e2e87 | 
| 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  |