>> At the moment I am thinking whether the old approach of checking
>> everything except the computations can be restored without using fancy
>> low-level stuff.  Maybe by a locale.
> This is indeed a bit fragile. I used to make manual tests of
> Flyspeck-Tame over some time, but now ignore that problem.
> Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base"
> that does everything except the actual "eval" steps, and postpone the
> checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ...

Something like that indeed.  A completeness proof relative to a locale
which has the computational results as assumption apt for later


Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to