[isabelle-dev] Primzahlen in Isabelle

[Amine Chaieb]

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.

Aemin.
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