[isabelle] isar-ref: simpset ~> Proof.context

A minor thing I just noticed: In isar-ref (page 212) it is written

  The implementation, which is provided as ML source
  text, needs to be of type
  morphism -> simpset -> cterm -> thm option

but it should be

   morphism -> Proof.context -> cterm -> thm option



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