| author | wenzelm | 
| Mon, 27 Feb 2012 16:56:25 +0100 | |
| changeset 46711 | f745bcc4a1e5 | 
| 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 |