src/Sequents/LK/Nat.thy
2014-02-01 wenzelm 2014-02-01 simplified sessions;
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;
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2010-12-20 wenzelm 2010-12-20 proper identifiers for consts and types;
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2007-05-09 wenzelm 2007-05-09 tuned ML setup;
2006-11-20 wenzelm 2006-11-20 converted legacy ML scripts;
2005-09-18 wenzelm 2005-09-18 converted to Isar theory format;
1999-07-28 paulson 1999-07-28 congruence rule for |-, etc.
1999-07-27 paulson 1999-07-27 fixed the comments...
1999-07-27 paulson 1999-07-27 Sequents/LK/Nat: new example of simplification in LK