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


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?

Christian Doczkal

Attachment: smime.p7s
Description: S/MIME cryptographic signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.