changeset 39302 | d7728f65b353 |
parent 39199 | 720112792ba0 |
child 39967 | 1c6dce3ef477 |
--- a/src/HOLCF/Algebraic.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOLCF/Algebraic.thy Mon Sep 13 11:13:15 2010 +0200 @@ -446,7 +446,7 @@ apply (clarify, simp add: fd_take_fixed_iff) apply (simp add: finite_fixes_approx) apply (rule inj_onI, clarify) -apply (simp add: set_ext_iff fin_defl_eqI) +apply (simp add: set_eq_iff fin_defl_eqI) done lemma fd_take_covers: "\<exists>n. fd_take n a = a"