src/HOL/Tools/res_reconstruct.ML
2009-05-04 immler 2009-05-04 added Philipp Meyer's implementation of AtpMinimal together with related changes in the sledgehammer-interface: adapted type of prover, optional relevance filtering, public get_prover for registered atps in AtpManager, included atp_minimize in s/h response;
2009-04-04 immler 2009-04-04 reverted to explicitly check the presence of a refutation (compare to 479a2fce65e6); simplified handling of errors in remote script
2009-04-02 nipkow 2009-04-02 Updated to corrected E output messages
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-21 immler 2009-01-21 tuned; really find failure
2009-01-20 immler 2009-01-20 modified remote script; modified handling of errors
2008-12-31 wenzelm 2008-12-31 use regular Term.add_XXX etc.;
2008-12-31 wenzelm 2008-12-31 use exists_subterm directly; moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-10-13 wenzelm 2008-10-13 ** Update from Fabian ** reset print mode when producing proof text;
2008-10-03 wenzelm 2008-10-03 version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
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