author | haftmann |
Mon, 15 Jun 2009 08:16:08 +0200 | |
changeset 31636 | 138625ae4067 |
parent 29249 | 4dc278c8dc59 |
child 35762 | af3ff2ba4c54 |
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:
5
diff
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 |