Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Aug 22 2022 at 12:59):

From: Christian Sternagel <c.sternagel@gmail.com>
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


Last updated: Mar 29 2024 at 04:18 UTC