Re: [isabelle] Proof help on Cardinality and list_all2



On 07.05.2012 20:06, Aaron W. Hsu wrote:
    show ?thesis
      by (simp add: eq_cart card_image subset_inj_on[OF inj]
                    card_cartesian_product)
qed

What is the OF here?  I understand the other elements, but what does the
subset_inj_on[OF inj] part do?

A[OF B] discharges the first premise of A with B.

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.