Re: [isabelle] unhelpful comment in Term.ML



Am 11.11.2015 um 11:17 schrieb Makarius:


In general, Isabelle sources are understood as follows (in that order):

  (1) reading the definition in ML

  (2) looking through typical uses in ML

  (3) peeking at the informal snippets around the formal text, without
      taking them too seriously

Note that good software engineering practices would imply the opposite order.

Best, Till




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