| changeset 55465 | 0d31c0546286 |
| parent 55413 | a8e96847523c |
| child 58880 | 0baae4311a9f |
--- a/src/HOL/HOLCF/Library/List_Cpo.thy Fri Feb 14 07:53:45 2014 +0100 +++ b/src/HOL/HOLCF/Library/List_Cpo.thy Fri Feb 14 07:53:45 2014 +0100 @@ -242,7 +242,7 @@ using f apply (simp add: prod_cont_iff) apply (rule cont_apply [OF g]) -apply (rule list_contI, rule map.simps, simp, simp, simp) +apply (rule list_contI, rule list.map, simp, simp, simp) apply (induct_tac y, simp, simp) done