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
> 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?
> Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and