>> 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
interpretation.
Florian
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
