Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bug? Or still just confusing correct behavior?

view this post on Zulip Email Gateway (Nov 21 2020 at 05:25):

From: Peter Reitinger <>

recently I posted correct, but confusing behavior about simplification on
terms with functions with "open type, I mean not explicitly specified". The
behavior of isabelle was still correct because my formula was actually a
set of formulae for each possible type specification if I understood

Anyway, the actual question in this mail is:

Would this be a real bug? Btw it was observed in the old version 2019...
I just want to clarify before I send the real bug or confusion report to
the right mailing list... ;-)

[image: image.png]

Best regards, and I still love Isabelle! ;-)

Peter Reitinger

Last updated: Sep 25 2021 at 08:21 UTC