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



Try ?a1.0 = "..."

Tobias

Christian Doczkal wrote:
> 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?
> 
> 





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