[isabelle] Augmenting facts



Hello all

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?

Any help will be appreciated!

John





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