Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright 1992 University of Cambridge
6 Natural numbers in Zermelo-Fraenkel Set Theory
12 nat_case :: "[i, i=>i, i]=>i"
13 nat_rec :: "[i, i, [i,i]=>i]=>i"
17 nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
20 "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
24 \ wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"