> This theory takes quite a while to load, and I have found out why:
>
> text{* A bit of regression testing: *}
>
> lemma "prime(97::nat)" by simp
> lemma "prime(997::nat)" by eval
>
> The proof that 97 is prime takes 35 seconds on a very fast machine. Can we
> get rid of this or at least substitute a smaller number?
The question is whether this has really to be performed using simp.
As an alternative, a suitable code equations could be proven using the
primes_upto in Eratosthenes.thy, but I did never take any measurements
at which threshold the additional data structures outperform brute-force
calculation.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
