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
     THEN
     auto_tac (cs, ss)

Jasmin






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