Broken AFP/SCL_Simulates_Ground_Resolution

Makarius makarius at sketis.net
Sat Jan 11 21:34:57 CET 2025


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