| changeset 10216 | e928bdf62014 |
| parent 9907 | 473a6604da94 |
| child 12089 | 34e7693271a9 |
--- a/src/ZF/Trancl.ML Fri Oct 13 10:49:05 2000 +0200 +++ b/src/ZF/Trancl.ML Fri Oct 13 11:15:56 2000 +0200 @@ -19,7 +19,7 @@ qed "rtrancl_mono"; (* r^* = id(field(r)) Un ( r O r^* ) *) -bind_thm ("rtrancl_unfold", rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_Tarski)); +bind_thm ("rtrancl_unfold", rtrancl_bnd_mono RS (rtrancl_def RS def_lfp_unfold)); (** The relation rtrancl **)