Problems in AFP

[Florian Haftmann]

> Padic_Ints FAILED (see also "isabelle build_log -H Error Padic_Ints")
> *** Failed to finish proof (line 566 of "$AFP/Padic_Ints/Padic_Integers.thy"):
> *** goal (1 subgoal):
> ***  1. ⟦2 ≤ n; 1 ≤ (2::?'a3) ⟹ (4::?'a3) ≤ (2::?'a3) ^ n⟧
> ***     ⟹ 4 ≤ 2 ^
> ***            n
> *** At command "by" (line 566 of "$AFP/Padic_Ints/Padic_Integers.thy")

> CVP_Hardness FAILED (see also "isabelle build_log -H Error CVP_Hardness")
> *** Undefined fact: "linordered_semidom_class.power_mono" (line 320 of "$AFP/CVP_Hardness/CVP_p.thy")
> *** At command "by" (line 320 of "$AFP/CVP_Hardness/CVP_p.thy")

> Coppersmith_Method FAILED (see also "isabelle build_log -H Error Coppersmith_Method")
> *** Undefined fact: "linordered_semidom_class.power_mono" (line 115 of "$AFP/Coppersmith_Method/Howgrave_Graham.thy")
> *** At command "by" (line 115 of "$AFP/Coppersmith_Method/Howgrave_Graham.thy")

> *** Timeout
> Schoenhage_Strassen FAILED (see also "isabelle build_log -H Error Schoenhage_Strassen")

	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250502/19ee4065/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250502/19ee4065/attachment.sig>