| author | wenzelm | 
| Thu, 27 Mar 2008 15:32:19 +0100 | |
| changeset 26436 | dfd6947ab5c2 | 
| parent 26058 | 279016aebc41 | 
| child 29223 | e09c53289830 | 
| permissions | -rw-r--r-- | 
| 12175 | 1 | (* Title: ZF/ROOT.ML | 
| 6 
8ce8c4d13d4d
Installation of new simplifier for ZF.  Deleted all congruence rules not
 lcp parents: 
5diff
changeset | 2 | ID: $Id$ | 
| 1461 | 3 | Author: Lawrence C Paulson, Cambridge University Computer Laboratory | 
| 0 | 4 | Copyright 1993 University of Cambridge | 
| 5 | ||
| 12175 | 6 | Zermelo-Fraenkel Set Theory on top of classical First-Order Logic. | 
| 7 | This theory is the work of Martin Coen, Philippe Noel and Lawrence | |
| 8 | Paulson. | |
| 0 | 9 | *) | 
| 10 | ||
| 26058 | 11 | use_thys ["Main", "Main_ZFC"]; | 
| 0 | 12 |