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
additional facts.

Thanks
John

>
> TIA
>
> John
>
>> Hope this helps,
>> Alex
>>
>





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