[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

cheers

chris





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