Email Gateway (Nov 21 2020 at 05:25): Email Gateway (Nov 21 2020 at 05:25):From: Peter Reitinger <peter.reitinger@gmail.com>
Hi,
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
correctly.
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
image.png
Last updated: Jul 15 2022 at 23:21 UTC