src/Sequents/LK.thy
2016-07-20 wenzelm 2016-07-20 tuned;
2015-10-10 wenzelm 2015-10-10 more symbols;
2015-10-10 wenzelm 2015-10-10 more symbols;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-02-01 wenzelm 2014-02-01 method_setup "lem";
2014-02-01 wenzelm 2014-02-01 proper Simplifier method setup;
2014-02-01 wenzelm 2014-02-01 misc tuning and modernization;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-06-11 wenzelm 2008-06-11 converted ML proofs from simpdata.ML; tuned;
2006-11-21 wenzelm 2006-11-21 removed legacy ML setup;
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)