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?
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)+
... 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