src/HOL/Library/Product_Order.thy
changeset 56154 f0a927235162
parent 54776 db890d9fc5c2
child 56166 9a241bc276cd
     1.1 --- a/src/HOL/Library/Product_Order.thy	Sat Mar 15 03:37:22 2014 +0100
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Sat Mar 15 08:31:33 2014 +0100
     1.3 @@ -225,10 +225,10 @@
     1.4  by (auto simp: Sup_prod_def SUP_def)
     1.5  
     1.6  lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
     1.7 -by (auto simp: INF_def Inf_prod_def image_compose)
     1.8 +by (auto simp: INF_def Inf_prod_def image_comp)
     1.9  
    1.10  lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
    1.11 -by (auto simp: SUP_def Sup_prod_def image_compose)
    1.12 +by (auto simp: SUP_def Sup_prod_def image_comp)
    1.13  
    1.14  lemma INF_prod_alt_def:
    1.15    "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"