Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Relation.ImageP?

view this post on Zulip Email Gateway (Aug 19 2022 at 14:59):

From: Joachim Breitner <breitner@kit.edu>
Hello,

I was just looking for a predicate version of Relation.Image, but could
not find one, while most other definitions are available for both. Is
that a deliberate mission?

Greetings,
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 15:00):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Joachim,

I do not thing that omission is deliberate. You will find more missing
twins.

Generally, the relation material in HOL-Main stems from very different
Isabelle epochs could profit from some consolidation (uniform naming
conventions etc.) .

Florian
signature.asc

Last updated: Apr 26 2024 at 20:16 UTC