--- a/src/ZF/Constructible/Relative.thy Tue Jul 30 11:38:33 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Tue Jul 30 11:39:57 2002 +0200
@@ -746,7 +746,7 @@
(*NOT for the simplifier. The assumption M(z') is apparently necessary, but
causes the error "Failed congruence proof!" It may be better to replace
is_nat_case by nat_case before attempting congruence reasoning.*)
-lemma (in M_triv_axioms) is_nat_case_cong:
+lemma is_nat_case_cong:
"[| a = a'; k = k'; z = z'; M(z');
!!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |]
==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')"