| changeset 10216 | e928bdf62014 |
| parent 9907 | 473a6604da94 |
| child 12552 | d2d2ab3f1f37 |
--- a/src/ZF/Nat.ML Fri Oct 13 10:49:05 2000 +0200 +++ b/src/ZF/Nat.ML Fri Oct 13 11:15:56 2000 +0200 @@ -14,7 +14,7 @@ qed "nat_bnd_mono"; (* nat = {0} Un {succ(x). x:nat} *) -bind_thm ("nat_unfold", nat_bnd_mono RS (nat_def RS def_lfp_Tarski)); +bind_thm ("nat_unfold", nat_bnd_mono RS (nat_def RS def_lfp_unfold)); (** Type checking of 0 and successor **)