src/HOL/Tools/res_reconstruct.ML
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