src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 61424 c3658c18b7bc
parent 58880 0baae4311a9f
child 62175 8ffc4d0e652d
     1.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -465,7 +465,7 @@
     1.4    "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
     1.5      = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
     1.6  apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
     1.7 -apply (simp only: map_apply_thms pair_collapse)
     1.8 +apply (simp only: map_apply_thms prod.collapse)
     1.9  apply (simp only: fix_def2)
    1.10  apply (rule lub_eq)
    1.11  apply (rule nat.induct)