src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
Tue, 31 Mar 2015 19:39:05 +0200 wenzelm tuned -- avoid exotic Name_Space.defined_entry;
Mon, 30 Mar 2015 22:34:59 +0200 wenzelm support for strictly private name space entries;
Mon, 23 Mar 2015 13:30:59 +0100 wenzelm support 'for' fixes in rule_tac etc.;
Fri, 20 Mar 2015 14:48:04 +0100 wenzelm tuned signature;
Fri, 20 Mar 2015 11:23:32 +0100 wenzelm tuned;
Thu, 19 Mar 2015 22:30:57 +0100 wenzelm more position information;
Fri, 06 Mar 2015 23:54:36 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Wed, 11 Feb 2015 18:16:33 +0100 wenzelm proper context;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sat, 08 Nov 2014 12:15:40 +0100 wenzelm more direct type equality;
Sun, 21 Sep 2014 20:14:04 +0200 wenzelm more standard Isabelle/ML operations;
Sun, 21 Sep 2014 19:53:50 +0200 wenzelm tuned;
Sun, 22 Jun 2014 06:16:57 +0100 sultana Metis is being used to emulate E steps;
Sat, 22 Mar 2014 18:15:09 +0100 wenzelm more antiquotations;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Wed, 19 Mar 2014 22:10:33 +0100 wenzelm more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
Wed, 19 Feb 2014 15:57:02 +0000 sultana added a function that carries out all the reconstruction steps, for improved usability;
Wed, 19 Feb 2014 15:57:02 +0000 sultana reconstruction framework for LEO-II's TPTP proofs;
less more (0) tip