Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Exception- ERROR "congc result" raised

view this post on Zulip Email Gateway (Aug 17 2022 at 14:49):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
Does anyone know what this error message means ?

thanks for ny help

Jeremy

view this post on Zulip Email Gateway (Aug 17 2022 at 14:49):

From: Lawrence Paulson <lp15@cam.ac.uk>
It may be a simplifier bug: I see that this message appears in Pure/
meta_simplifier.ML.

Do you have a small example that triggers it?

Larry

Last updated: Nov 21 2024 at 12:39 UTC