src/HOL/BNF_Cardinal_Arithmetic.thy
changeset 55866 a6fa341a6d66
parent 55851 3d40cf74726c
child 56191 159b0c88b4a4
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 12:48:20 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -351,13 +351,13 @@
     1.4  by (blast intro: cinfinite_cprod2 Card_order_cprod)
     1.5  
     1.6  lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
     1.7 -by (metis cprod_mono ordIso_iff_ordLeq)
     1.8 +unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono)
     1.9  
    1.10  lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
    1.11 -by (metis cprod_mono1 ordIso_iff_ordLeq)
    1.12 +unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono1)
    1.13  
    1.14  lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
    1.15 -by (metis cprod_mono2 ordIso_iff_ordLeq)
    1.16 +unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono2)
    1.17  
    1.18  lemma cprod_com: "p1 *c p2 =o p2 *c p1"
    1.19  by (simp only: cprod_def card_of_Times_commute)