Re: [isabelle] stuck on proof



On 17.08.2010 10:07, Tobias Nipkow wrote:
> lemma "(principalType e = Some t) ==>  (STyping e t)"
> apply (induct e arbitrary: t)
> apply (auto simp: STyping.intros split:option.splits SType.splits)
> done

As I often forget about *.intros and similar sets: find_theorems has a with_dups option, which shows you also these alternate names.

  -- Lars





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