src/Sequents/LK0.thy
2015-10-10 wenzelm 2015-10-10 more symbols;
2015-10-10 wenzelm 2015-10-10 more symbols;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2015-07-23 wenzelm 2015-07-23 isabelle update_cartouches;
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-03-23 wenzelm 2015-03-23 support 'for' fixes in rule_tac etc.;
2015-03-20 wenzelm 2015-03-20 tuned signature;
2015-03-19 wenzelm 2015-03-19 more position information;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-11-01 wenzelm 2014-11-01 eliminated spurious semicolons;
2014-02-10 wenzelm 2014-02-10 prefer vacuous definitional type classes over axiomatic ones;
2014-02-01 wenzelm 2014-02-01 method_setup "lem";
2014-02-01 wenzelm 2014-02-01 misc tuning and modernization;
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-02-28 wenzelm 2013-02-28 eliminated legacy 'axioms';
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-05-15 wenzelm 2011-05-15 simplified/unified method_setup/attribute_setup;
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-08-17 haftmann 2010-08-17 deglobalization
2010-04-28 wenzelm 2010-04-28 renamed command 'defaultsort' to 'default_sort';
2010-03-01 haftmann 2010-03-01 merged
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-24 wenzelm 2010-02-24 modernized syntax declarations, and make them actually work with authentic syntax;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-14 wenzelm 2008-06-14 proper context for tactics derived from res_inst_tac;
2008-06-11 wenzelm 2008-06-11 more antiquotations;
2007-05-09 wenzelm 2007-05-09 eliminated unnamed infixes;
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation;
2006-11-21 wenzelm 2006-11-21 removed legacy 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;
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-21 wenzelm 2004-05-21 proper use of 'syntax';
2004-04-14 kleing 2004-04-14 use more symbols in HTML output
2002-01-08 wenzelm 2002-01-08 syntax "_not_equal";
2001-11-09 wenzelm 2001-11-09 got rid of obsolete input filtering;
1999-08-03 paulson 1999-08-03 Sara Kalvala: moving the <<...>> notation from LK to Sequents
1999-07-28 paulson 1999-07-28 adding missing declarations for the <<...>> notation
1999-07-27 paulson 1999-07-27 renamed theory LK to LK0