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



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.






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