[isabelle-dev] Failure of AFP/Polylog

Makarius makarius at sketis.net
Tue Mar 12 17:13:03 CET 2024


We currently have a failure of AFP/Polylog, using Isabelle/1e7b5a258bc5 + 
AFP/dbd87cb0c2b5.

This is probably related to changes to "meromorphic_on" here:

changeset:   79857:819c28a7280f
user:        paulson <lp15 at cam.ac.uk>
date:        Mon Mar 11 15:07:02 2024 +0000
files:       src/HOL/Analysis/Analysis.thy 
src/HOL/Analysis/Complex_Analysis_Basics.thy src/HOL/Analysis/Complex_Trans
cendental.thy src/HOL/Analysis/Gamma_Function.thy 
src/HOL/Analysis/Sparse_In.thy src/HOL/Complex_Analysis/Meromorphic.
thy src/HOL/Deriv.thy src/HOL/Nat.thy
description:
New material by Wenda Li and Manuel Eberl


	Makarius


More information about the isabelle-dev mailing list