[isabelle] propositional calculi equivalence



Hi,
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
logic)?
I hope I'm making myself clear. Any pointers would be appreciated.
Thanks in advance,
-- 
 Hector





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