Re: [isabelle] Augmenting facts
>> 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?
Just some further information: I'd like to apply the auto_tac with
>> Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and