Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Tactic corresponding to an Eisbach "method"

Email Gateway (Aug 22 2022 at 16:09):

From: Cristina Matache <cristina@aestheticintegration.com>
Dear Eisbach experts,

I defined an Eisbach "method" that I'm using in some Isar proofs, but I
would also like to access the corresponding tactic at the Isabelle/ML level.

I need to get hold of an ML function that is similar to, say blast_tac, but
corresponds to my custom Eisbach method. Is there a way to do this?
I would prefer not to write my tactic directly in Isabelle/ML because
Eisbach methods are much easier to understand and manage for me.

Thanks,
Cristina

Last updated: Apr 19 2024 at 08:19 UTC