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