Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Tactic Emulation

Email Gateway (Aug 18 2022 at 10:20):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Christian Urban wrote:
You may also note that recent development snapshots of Isabelle support
a bundle of antiquotations on the Isar ML-level, notably an
antiquotation for theorems:

lemma True
by (tactic {* rtac @{thm TrueI} 1 *} )

I.e. there is no need for explicit ML bindings for theorems any more.

Florian
florian.haftmann.vcf
signature.asc

Last updated: May 03 2024 at 04:19 UTC