[isabelle] Extensive case splits


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)

where each application of this little sequence of commands takes between
1 and 30 secs. I am currently wondering if it is possible to speed up
the process of proving the single goals by remembering the successful
tactic of the previous step and all automatically added theorems of it.
Especially since the proofs of many sub-goals look quite similar. Any
speedup would help, especially since there are goals that need to be
split up into about 23k cases to solve them. 


Dominik Luecke                 Phone +49-421-218-64265
Dept. of Computer Science      Fax   +49-421-218-9864265
University of Bremen           luecke at tzi.de           
P.O.Box 330440, D-28334 Bremen
PGP-Key ID 0x2D82571B

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