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