Re: [isabelle] Augmenting facts



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
state?

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).

Hope this helps,
Alex





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