src/FOL/ex/cla.ML
1997-03-04 paulson 1997-03-04 Updated reference to Pelletier erratum
1997-02-14 paulson 1997-02-14 Added a new challenge problem
1997-02-10 paulson 1997-02-10 Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int
1997-01-31 paulson 1997-01-31 Correction to Problem 24
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-08-19 paulson 1996-08-19 Improved the proof of Problem 38
1996-06-17 paulson 1996-06-17 Inserted comment about problem 43
1996-04-04 paulson 1996-04-04 deleted obsolete comment
1996-03-11 paulson 1996-03-11 Added formulation of Halting Problem
1996-01-30 clasohm 1996-01-30 fixed typo
1996-01-29 clasohm 1996-01-29 expanded tabs
1995-12-14 paulson 1995-12-14 Added Pelletier's problem 62, as corrected in AAR Newletter #31
1994-11-24 lcp 1994-11-24 updated for new deepen_tac
1994-10-31 lcp 1994-10-31 FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
1994-10-19 lcp 1994-10-19 FOL/ex/cla/58: slightly shorter proof
1994-07-27 lcp 1994-07-27 added a new example due to Robin Arthan
1994-06-17 lcp 1994-06-17 problem 38 is provable
1993-10-07 lcp 1993-10-07 examples now use ~= for "not equals"
1993-09-24 lcp 1993-09-24 Added example from Avron: Gentzen-Type Systems, Resolution and Tableaux, JAR 10
1993-09-16 clasohm 1993-09-16 Initial revision