src/Sequents/LK.thy
2005-09-18 wenzelm 2005-09-18 converted to Isar theory format;
1999-07-28 paulson 1999-07-28 congruence rule for |-
1999-07-27 paulson 1999-07-27 a new theory containing just an axiom needed to derive imp_cong
1999-04-20 paulson 1999-04-20 IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly) provided HIGHER-ORDER logic
1997-10-10 wenzelm 1997-10-10 fixed dots;
1996-10-09 paulson 1996-10-09 New unified treatment of sequent calculi by Sara Kalvala combines the old LK and Modal with the new ILL (Int. Linear Logic)