See if we can run IsaCoSy without proving termination. We might be able
to do this by using "sorry" as our termination proof ("oops" will cause
Isabelle to ignore the proof obligation *and* ignore the definition; we
want it to keep the definition but 'cheat' the proof).