Re: [isabelle] Problem instantiating variables of form ?a1.0
Try ?a1.0 = "..."
Christian Doczkal wrote:
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and