Re: [isabelle] Augmenting facts
Am 29.09.2010 um 14:13 schrieb John Munroe:
>>> 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
> additional facts.
If the facts have no particular form, you can add them as assumptions using Method.insert_tac. E.g.
Method.insert_tac my_extra_facts 1
auto_tac (cs, ss)
This archive was generated by a fusion of
Pipermail (Mailman edition) and