*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Problem instantiating variables of form ?a1.0*From*: Christian Doczkal <c.doczkal at stud.uni-saarland.de>*Date*: Sun, 26 Oct 2008 16:45:24 +0100

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? -- Regards Christian Doczkal

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Problem instantiating variables of form ?a1.0***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] export .thy files as xml
- Next by Date: [isabelle] Problem instantiating variables of form ?a1.0
- Previous by Thread: Re: [isabelle] export .thy files as xml
- Next by Thread: Re: [isabelle] Problem instantiating variables of form ?a1.0
- Cl-isabelle-users October 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list