[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

Any help will be appreciated!


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