Re: [isabelle] Baffling behavior: unable to prove P=>P



Am Mittwoch, den 27.08.2014, 23:23 +0100 schrieb Holden Lee:
> card {l. l = [] ∧ (∀n∈set l. n = 0)} = Suc 0

Btw, you can proof this with the simplifier by:

  simp cong: conj_cong

Then 

  {l. l = [] ∧ (∀n∈set l. n = 0)}
     = with conj_cong
  {l. l = [] ∧ (∀n∈set []. n = 0)}
     =
  {[]}

 - Johannes






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