src/Sequents/LK.thy
Wed, 20 Jul 2016 20:24:21 +0200 wenzelm tuned;
Sat, 10 Oct 2015 20:54:44 +0200 wenzelm more symbols;
Sat, 10 Oct 2015 20:51:39 +0200 wenzelm more symbols;
Thu, 23 Jul 2015 14:25:05 +0200 wenzelm isabelle update_cartouches;
Sat, 18 Jul 2015 20:54:56 +0200 wenzelm prefer tactics with explicit context;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sat, 01 Feb 2014 18:22:38 +0100 wenzelm method_setup "lem";
Sat, 01 Feb 2014 18:05:03 +0100 wenzelm proper Simplifier method setup;
Sat, 01 Feb 2014 17:56:03 +0100 wenzelm misc tuning and modernization;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Sun, 20 Nov 2011 20:15:02 +0100 wenzelm eliminated obsolete "standard";
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Fri, 20 Mar 2009 15:24:18 +0100 wenzelm eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
Wed, 03 Dec 2008 15:58:44 +0100 haftmann made repository layout more coherent with logical distribution structure; stripped some $Id$s
Wed, 11 Jun 2008 15:41:33 +0200 wenzelm converted ML proofs from simpdata.ML;
Tue, 21 Nov 2006 00:07:05 +0100 wenzelm removed legacy ML setup;
Sun, 18 Sep 2005 15:20:08 +0200 wenzelm converted to Isar theory format;
Wed, 28 Jul 1999 13:45:33 +0200 paulson congruence rule for |-
Tue, 27 Jul 1999 18:52:48 +0200 paulson a new theory containing just an axiom needed to derive imp_cong
Tue, 20 Apr 1999 14:38:17 +0200 paulson IMPORTANT CHANGE: declares class "term". Previously LK (incorrectly)
Fri, 10 Oct 1997 18:17:17 +0200 wenzelm fixed dots;
Wed, 09 Oct 1996 13:32:33 +0200 paulson New unified treatment of sequent calculi by Sara Kalvala
less more (0) tip