Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem instantiating variables of form ?a1.0

view this post on Zulip Email Gateway (Aug 18 2022 at 12:34):

From: urban@math.lmu.de
Hi Christian,

Try

apply(rule_tac ?a1.0="..." in my_rule)

where a question-mark is in front of the
variable.

Hope this helps,
Christian

This message was sent using IMP, the Internet Messaging Program.

Last updated: Apr 05 2026 at 20:36 UTC