Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Standardized notation <# -> \<subset>#


view this post on Zulip Email Gateway (Aug 22 2022 at 15:06):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi Florian,

This change went a little bit too far:

changeset: 64587:8355a6e2df79
user: haftmann
date: Sat Dec 17 15:22:13 2016 +0100
summary: standardized notation

I think this was intended to improve the notation of multisets. In HOL-Algebra, <#, #> and <#> are used to denote cosets. <# and <#> were accidentally replaced by \<subset># and \<subset>#>. Could you please fix that?

Thanks

Clemens

view this post on Zulip Email Gateway (Aug 22 2022 at 15:06):

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

thanks for reporting this.

I will look after it.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 15:06):

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

see now
signature.asc


Last updated: Nov 21 2024 at 12:39 UTC