Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [isabelle-dev] HOL iff notation


view this post on Zulip Email Gateway (Aug 19 2022 at 11:57):

From: Gottfried Barrow <gottfried.barrow@gmx.com>
Dear Devs,

Users' interests should be properly represented. Users can actually
become quite interested in foundational features, and find uses for
low-level features that they are given access to. And once momentum
builds for features to be eliminated in a software product, it's can be
hard to stop, so it pays to complain early.

The quotes below from the dev list provide some context. I'll make this
a short comment, in case nothing more is required.

I care about the operator "==", and over the months, Makarius has made a
number of comments deemphasizing it, and the comments below indicate
something similar. I don't see how "==" could be gotten rid of from
Isar, but what do I know?

The operator "==" will forever be an Isar operator, won't it? It's not
going away, is it? No reply is necessary if it's not going away. I would
appreciate a reply if it's going away, so I can become irate now.

Thanks,
GB

https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2013-September/004527.html


Last updated: Mar 28 2024 at 08:18 UTC