src/FOL/IFOL.ML
1998-07-14 paulson 1998-07-14 stac now uses CHANGED_GOAL and correctly fails when it has no useful effect, even for conditional rewrites
1997-12-22 paulson 1997-12-22 New rules rev_iffD{1,2}
1997-11-07 oheimb 1997-11-07 added contrapos
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-09-29 paulson 1997-09-29 qed_spec_mp, normalize_thm, etc. copied in from HOL.ML
1997-03-27 paulson 1997-03-27 Updated comment
1996-09-26 paulson 1996-09-26 Declared stac
1996-07-26 paulson 1996-07-26 Addition of rev_notE
1996-03-26 paulson 1996-03-26 Added two of KGs rules
1996-01-29 clasohm 1996-01-29 expanded tabs
1995-10-13 clasohm 1995-10-13 corrected spelling of title
1995-04-06 lcp 1995-04-06 Fixed typo.
1994-12-23 lcp 1994-12-23 Added Krzysztof's theorem disj_imp_disj
1994-12-16 lcp 1994-12-16 conj_cong2: new congruence rule
1994-12-13 clasohm 1994-12-13 removed FOL_Lemmas and IFOL_Lemmas; added qed_goal
1993-09-24 lcp 1993-09-24 Added ex_ex1I: new introduction rule for the EX! quantifier.
1993-09-16 clasohm 1993-09-16 Initial revision