| author | wenzelm |
| Sun, 29 Jul 2007 22:42:00 +0200 | |
| changeset 24067 | 69b51bc5ce06 |
| parent 23894 | 1a4167d761ac |
| child 25750 | 4e796867ccb5 |
| 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 |
||
11 |
val banner = "ZF Set Theory (in FOL)"; |
|
12 |
writeln banner; |
|
13 |
||
| 23146 | 14 |
use_thy "Main_ZFC"; |