[isabelle] propositional calculi equivalence

I just came to Isabelle after having learnt some functional
programming through SML. Now I'm teaching myself some mathematical
logic (back to the foundations!). My question is: how to use Isabelle
to establish the equivalence of different propositional calculi, say
Hilbert-style vs. LK sequent calculus (restricted to propositional
I hope I'm making myself clear. Any pointers would be appreciated.
Thanks in advance,

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