[isabelle-dev] Primzahlen in Isabelle

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sat Dec 1 18:39:32 CET 2007


Amine Chaieb schrieb:
> Zur Antwort auf der Gestern gestellte Frage: was ist die bis jetzt 
> groesste Zahl von der wir Primalitaet zeigen koennen:
> 
> val it =
>     "prime
>  
> 259117086013202627776246767922441530941818887553125427303974923161874019266586362086201209516800483406550695241733194177441689509238807017410377709597512042313066624082916353517952311186154862265604547691127595848775610568757931191017711408826252153849035830401185072116424747461823031471398340229288074545677907941037288235820705892351068433882986888616658650280927692080339605869308790500409503709875902119018371991620994002568935113136548829739112656797303241986517250116412703509705427773477972349821676443446668383119322540099648994051790241624056519054483690809616061625743042361721863339415852426431208737266591962061753535748892894599629195183082621860853400937932839420261866586142503251450773096274235376822938649407127700846077124211823080804139298087057504713825264571448379371125032081826126566649084251699453951887789613650248405739378594599444335231188280123660406262468609212150349937584782292237144339628858485938215738821232393687046160677362909315071"
>       [!] : Thm.thm
> ML>

Is it an LCF thm or did you use an evaluation oracle?

	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 249 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20071201/40f3e1d8/attachment.sig>


More information about the isabelle-dev mailing list