Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 12:34):

From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello

I have an (automatically generated; large) rule which has meta variables
of the form ?a1.0 ?a2.0 .. and I seem to be unable to instantiate
these variables.

If i try

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

I get a syntax error at the "." and if I try

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

it says that there is no such variable in the theorem. So how does one
instantiate this kind of variables?
smime.p7s

Email Gateway (Aug 18 2022 at 12:34):

From: Tobias Nipkow <nipkow@in.tum.de>
Try ?a1.0 = "..."

Tobias

Christian Doczkal wrote:

Last updated: May 03 2024 at 08:18 UTC