[isabelle] isabelle doc classes: c_class ~> (class.)c?



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.