Re: [isabelle] Extensive case splits

This sort of case-splitting easily gives rise to huge numbers of goals, but this is best done internally. I assume you have already tried auto and force on them?
Larry Paulson

On 6 Aug 2007, at 17:27, Dominik Luecke wrote:

I am currently trying to prove a theorems that involve lots of case
splits in the proof process. I mean the single sub-goals a solvable by

  apply (erule disjE)+
  apply (simp)
  apply (simp)

... Any speedup would help, especially since there are goals that need to be
split up into about 23k cases to solve them.

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