Email Gateway (Aug 22 2022 at 12:59): 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: Nov 21 2024 at 12:39 UTC