src/HOL/Tools/res_reconstruct.ML
Wed, 19 Dec 2007 23:10:17 +0100 wenzelm removed strange MacRoman character;
Wed, 19 Dec 2007 17:40:48 +0100 paulson Replaced refs by config params; finer critical section in mets method
Wed, 28 Nov 2007 16:26:03 +0100 paulson Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
Mon, 12 Nov 2007 21:09:32 +0100 wenzelm back to sigusr2, after Poly/ML 5.1 has been adapted;
Mon, 12 Nov 2007 20:10:34 +0100 wenzelm changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
Thu, 18 Oct 2007 17:34:27 +0200 paulson Improving the propagation of type constraints for Frees
Thu, 11 Oct 2007 15:59:31 +0200 paulson rationalized redundant code
Thu, 11 Oct 2007 10:23:09 +0200 paulson failure messages
Tue, 09 Oct 2007 18:14:00 +0200 paulson context-based treatment of generalization; also handling TFrees in axiom clauses
Tue, 09 Oct 2007 00:20:13 +0200 wenzelm generic Syntax.pretty/string_of operations;
Sun, 23 Sep 2007 22:23:27 +0200 wenzelm TypeInfer.constrain: canonical argument order;
Tue, 18 Sep 2007 17:53:37 +0200 paulson metis now available in PreList
Fri, 07 Sep 2007 15:35:25 +0200 paulson allow TVars during type inference
Thu, 06 Sep 2007 17:03:53 +0200 paulson Vampire structured proofs. Better parsing; some bug fixes.
Thu, 30 Aug 2007 22:35:34 +0200 wenzelm replaced ProofContext.infer_types by general Syntax.check_terms;
Fri, 24 Aug 2007 14:16:44 +0200 paulson Returning both a "one-line" proof and a structured proof
Tue, 21 Aug 2007 18:30:11 +0200 paulson Modified message for sendback
Wed, 08 Aug 2007 13:59:46 +0200 paulson Fixing the code to undo the function ascii_of
Tue, 17 Jul 2007 16:06:13 +0200 paulson Full sort information by default.
Fri, 29 Jun 2007 18:21:25 +0200 paulson bug fixes to proof reconstruction
Thu, 31 May 2007 01:25:24 +0200 wenzelm TextIO.inputLine: use present SML B library version;
Wed, 23 May 2007 14:52:12 +0200 paulson formatting
Thu, 19 Apr 2007 18:23:11 +0200 paulson trying to make single-step proofs work better, especially if they contain
Wed, 18 Apr 2007 21:30:14 +0200 wenzelm simplified ProofContext.infer_types(_pats);
Sun, 15 Apr 2007 14:31:49 +0200 wenzelm proper ProofContext.infer_types;
Thu, 29 Mar 2007 11:12:03 +0200 paulson Now checks for types-only clause before outputting.
Wed, 21 Mar 2007 13:58:36 +0100 paulson Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
Mon, 19 Mar 2007 15:57:20 +0100 paulson No label on "show"; tries to remove dependencies more cleanly
Fri, 09 Mar 2007 13:10:22 +0100 paulson First stab at reconstructing HO problems
Wed, 28 Feb 2007 12:51:46 +0100 paulson Now outputs metis calls
Sat, 20 Jan 2007 14:09:14 +0100 wenzelm Output.debug: non-strict;
Tue, 09 Jan 2007 18:12:59 +0100 paulson More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
Fri, 05 Jan 2007 13:36:32 +0100 paulson Proof.context now sent to watcher and used in type inference step of proof reconstruction
Thu, 04 Jan 2007 17:55:12 +0100 paulson improvements to proof reconstruction. Some files loaded in a different order
Wed, 03 Jan 2007 18:29:46 +0100 paulson Improvements to proof reconstruction. Now "fixes" is inserted
Wed, 03 Jan 2007 11:06:52 +0100 paulson Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
less more (0) tip