| changeset 10186 | 499637e8f2c6 |
| parent 10179 | 9d5678e6bf34 |
| child 10196 | 4d1af711cf7b |
--- a/src/HOL/Trancl.ML Wed Oct 11 00:03:22 2000 +0200 +++ b/src/HOL/Trancl.ML Wed Oct 11 09:09:06 2000 +0200 @@ -15,7 +15,7 @@ by (REPEAT (ares_tac [monoI, subset_refl, comp_mono, Un_mono] 1)); qed "rtrancl_fun_mono"; -bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_Tarski)); +bind_thm ("rtrancl_unfold", rtrancl_fun_mono RS (rtrancl_def RS def_lfp_unfold)); (*Reflexivity of rtrancl*) Goal "(a,a) : r^*";