Problems in AFP

[Florian Haftmann]

isabelle: 267db8c321c4 tip
afp: 2a810c4dd72c tip

Am 02.05.25 um 22:30 schrieb 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/302beaed/attachment-0001.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/302beaed/attachment-0001.sig>