changeset 19769 | c40ce2de2020 |
parent 19736 | d8d0f8f51d69 |
child 20807 | bd3b60f9a343 |
--- a/src/HOL/Library/While_Combinator.thy Sun Jun 04 10:52:47 2006 +0200 +++ b/src/HOL/Library/While_Combinator.thy Mon Jun 05 14:22:58 2006 +0200 @@ -130,7 +130,7 @@ apply (blast dest: monoD) apply (fastsimp intro!: lfp_lowerbound) apply (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset]) -apply (clarsimp simp add: inv_image_def finite_psubset_def order_less_le) +apply (clarsimp simp add: finite_psubset_def order_less_le) apply (blast intro!: finite_Diff dest: monoD) done