2008-03-19 paulson 2008-03-19 Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts Sledgehammer no longer produces structured proofs by default.
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2007-12-19 wenzelm 2007-12-19 removed strange MacRoman character;
2007-12-19 paulson 2007-12-19 Replaced refs by config params; finer critical section in mets method
2007-11-28 paulson 2007-11-28 Chained theorems are no longer mentioned in metis calls and (if used) they prevent the output of a structured proof.
2007-11-12 wenzelm 2007-11-12 back to sigusr2, after Poly/ML 5.1 has been adapted;
2007-11-12 wenzelm 2007-11-12 changed Posix.Signal.usr2 to Posix.Signal.usr1 to make it work with Poly/ML 5.1;
2007-10-18 paulson 2007-10-18 Improving the propagation of type constraints for Frees
2007-10-11 paulson 2007-10-11 rationalized redundant code
2007-10-11 paulson 2007-10-11 failure messages
2007-10-09 paulson 2007-10-09 context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-09-23 wenzelm 2007-09-23 TypeInfer.constrain: canonical argument order;
2007-09-18 paulson 2007-09-18 metis now available in PreList
2007-09-07 paulson 2007-09-07 allow TVars during type inference
2007-09-06 paulson 2007-09-06 Vampire structured proofs. Better parsing; some bug fixes.
2007-08-30 wenzelm 2007-08-30 replaced ProofContext.infer_types by general Syntax.check_terms;
2007-08-24 paulson 2007-08-24 Returning both a "one-line" proof and a structured proof
2007-08-21 paulson 2007-08-21 Modified message for sendback
2007-08-08 paulson 2007-08-08 Fixing the code to undo the function ascii_of
2007-07-17 paulson 2007-07-17 Full sort information by default. Race condition on successful proofs fixed.
2007-06-29 paulson 2007-06-29 bug fixes to proof reconstruction
2007-05-31 wenzelm 2007-05-31 TextIO.inputLine: use present SML B library version;
2007-05-23 paulson 2007-05-23 formatting
2007-04-19 paulson 2007-04-19 trying to make single-step proofs work better, especially if they contain abstraction functions. Uniform names for Skolem and Abstraction functions
2007-04-18 wenzelm 2007-04-18 simplified ProofContext.infer_types(_pats);
2007-04-15 wenzelm 2007-04-15 proper ProofContext.infer_types;
2007-03-29 paulson 2007-03-29 Now checks for types-only clause before outputting.
2007-03-21 paulson 2007-03-21 Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
2007-03-19 paulson 2007-03-19 No label on "show"; tries to remove dependencies more cleanly
2007-03-09 paulson 2007-03-09 First stab at reconstructing HO problems
2007-02-28 paulson 2007-02-28 Now outputs metis calls
2007-01-20 wenzelm 2007-01-20 Output.debug: non-strict; renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);
2007-01-09 paulson 2007-01-09 More compact proof reconstruction: lines having fewer than !min_deps dependences are folded into the rest of the proof.
2007-01-05 paulson 2007-01-05 Proof.context now sent to watcher and used in type inference step of proof reconstruction
2007-01-04 paulson 2007-01-04 improvements to proof reconstruction. Some files loaded in a different order
2007-01-03 paulson 2007-01-03 Improvements to proof reconstruction. Now "fixes" is inserted
2007-01-03 paulson 2007-01-03 Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction