[isabelle-dev] Primzahlen in Isabelle

Amine Chaieb 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?
> Steven

More information about the isabelle-dev mailing list