Broken AFP/SCL_Simulates_Ground_Resolution
Martin Desharnais
martin.desharnais at posteo.de
Sun Jan 12 11:16:42 CET 2025
Hi Makarius,
adapted the AFP entry to Isabelle-devel and AFP-devel.
changeset: 15198:9585bf0cf504
tag: tip
user: desharna
date: Sun Jan 12 10:58:53 2025 +0100
summary: backed out changeset e681bc604fb1 following dca39520060a
changeset: 15197:dca39520060a
user: desharna
date: Sun Jan 12 10:54:01 2025 +0100
summary: adapted SCL_Simulates_Ground_Resolution to Isabelle-devel
and afp-devel
Regards,
Martin
Am 2025-01-11 21:34 schrieb Makarius:
> We have a total existence failure of AFP, due to import of a
> non-existent theory.
>
> I have disabled the bad session for now, see also:
>
> changeset: 15168:e681bc604fb1
> tag: tip
> user: wenzelm
> date: Sat Jan 11 21:28:06 2025 +0100
> summary: disable SCL_Simulates_Ground_Resolution for now: import
> of missing theory Superposition_Calculus.Ground_Ctxt_Extra;
>
>
> Makarius
More information about the isabelle-dev
mailing list