[isabelle-dev] Primzahlen in Isabelle
chaieb at in.tum.de
Sat Dec 1 19:08:59 CET 2007
A verified certificate checker running in ML.
For large numbers I found out that the checking actually runs very fast,
so after all LCF would be maybe possible.
I use external software to find primary number decomposition and this
takes the most of the time.
Actually for the example I sent, it does not terminate on my machine and
I was forced to give the primenumber decomposition for the first step
(the rest works).
I can sent the sources to test with your oracle, but I used some tricks
for Code-generation too, so maybe it's not trivial.
Steven Obua wrote:
> Amine Chaieb wrote:
>> LCF? are you kidding?
> So how did you do it then ? How long did the check run? Where can I find
> the sources?
More information about the isabelle-dev