Re: [isabelle] Augmenting facts



On Tue, Sep 28, 2010 at 9:42 PM, Alexander Krauss <krauss at in.tum.de> wrote:
> Hi John,
>
>> I'm having my first attempt in writing a tactic and I'm trying to
>> translate 'using' in Isar into a tactic. Should I be using
>> proof.put_facts for this? If so, how do I retrieve the current proof
>> state?
>
> Unlike Isar proof methods, tactics operate only on the goal state and do not
> take chained facts. On that level you can simply pass additional facts as ML
> arguments. To provide a method to the user that takes chained facts, use
> Method.METHOD (see Pure/Isar/method.ML).
>

I see. But how do I pass additional facts as arguments? Which function
should I pass to?

TIA

John

> Hope this helps,
> Alex
>





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