[isabelle] instance theorems



Hello,

  How do you get at the theorems which prove the "instance" calls?
Eg. the proof term for

instance * :: (finite, finite) finite
proof
  show "finite (UNIV :: ('a ◊ 'b) set)"
  proof (rule finite_Prod_UNIV)
    show "finite (UNIV :: 'a set)" by (rule finite)
    show "finite (UNIV :: 'b set)" by (rule finite)
  qed
qed

Thanks,

Sean




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