src/Sequents/prover.ML
Sun, 12 Sep 2021 20:37:15 +0200 wenzelm more antiquotations;
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Wed, 27 Aug 2014 14:54:32 +0200 wenzelm more explicit Method.modifier with reported position;
Tue, 05 Aug 2014 12:01:32 +0200 wenzelm more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
Wed, 09 Apr 2014 12:22:57 +0200 wenzelm proper context for print_tac;
Sat, 01 Feb 2014 17:56:03 +0100 wenzelm misc tuning and modernization;
Tue, 17 Aug 2010 19:36:39 +0200 haftmann more antiquotations
Wed, 21 Oct 2009 12:09:37 +0200 haftmann curried inter as canonical list operation (beware of argument order)
Wed, 21 Oct 2009 08:14:38 +0200 haftmann dropped redundant gen_ prefix
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Tue, 21 Jul 2009 01:03:18 +0200 wenzelm proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Sat, 17 May 2008 13:54:30 +0200 wenzelm structure Display: less pervasive operations;
Mon, 26 Feb 2007 23:18:24 +0100 wenzelm moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
Tue, 21 Nov 2006 00:07:05 +0100 wenzelm removed legacy ML setup;
Tue, 10 Oct 2006 13:59:13 +0200 haftmann gen_rem(s) abandoned in favour of remove / subtract
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Fri, 17 Jun 2005 18:35:27 +0200 wenzelm accomodate change of TheoryDataFun;
Tue, 07 May 2002 14:26:32 +0200 wenzelm use eq_thm_prop instead of slightly inadequate eq_thm;
Wed, 28 Nov 2001 00:46:26 +0100 wenzelm theory data: removed obsolete finish method;
Fri, 09 Nov 2001 00:19:20 +0100 wenzelm theory data: finish method;
Mon, 02 Aug 1999 15:40:30 +0200 wenzelm cat_lines;
Wed, 28 Jul 1999 13:55:02 +0200 paulson renamed ...thm_pack... to ...pack...
Tue, 27 Jul 1999 19:01:46 +0200 paulson moved the modal prover to modal.ML; installed the prover using TheoryDataFun
Mon, 28 Dec 1998 17:03:47 +0100 paulson added new arg for print_tac
Fri, 19 Dec 1997 10:13:47 +0100 wenzelm adapted to new sort function;
Mon, 20 Oct 1997 11:39:29 +0200 wenzelm adapted to qualified names;
Tue, 22 Jul 1997 11:14:18 +0200 paulson Removal of the tactical STATE
Wed, 09 Oct 1996 13:32:33 +0200 paulson New unified treatment of sequent calculi by Sara Kalvala
less more (0) tip