Email Gateway (Aug 22 2022 at 16:51): Email Gateway (Aug 22 2022 at 16:51):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
in the Isabelle documentation for type classes, as far as I can tell,
the underlying locale of a class "c" is called "c_class". But, for example,
interpretation wellorder_class
does not work (in Isabelle2017), while
interpretation wellorder
does (showing a subgoal involving the constant "class.wellorder"). Maybe
this chage could be reflected in the documentation.
cheers
chris
Last updated: Apr 25 2024 at 12:23 UTC