src/HOL/Lambda/ParRed.ML
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1996-11-04 nipkow 1996-11-04 Used nat_trans_tac. New Eta. various smaller changes.
1996-10-07 paulson 1996-10-07 Ran expandshort
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-11 nipkow 1996-09-11 Removed refs to clasets like rel_cs etc. Used implicit claset.
1996-05-07 paulson 1996-05-07 Updated for new form of induction rules
1996-02-09 nipkow 1996-02-09 Introduced qed_spec_mp.
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-02 nipkow 1996-01-02 Polished proofs.
1995-10-22 nipkow 1995-10-22 Improved a few proofs.
1995-10-06 nipkow 1995-10-06 New version with eta reduction.
1995-10-04 clasohm 1995-10-04 added local simpsets
1995-06-29 nipkow 1995-06-29 Renamed some vars.
1995-06-23 nipkow 1995-06-23 Put in direct proof of C-R w/o detour via cd.
1995-05-22 nipkow 1995-05-22 Polished the presentation making it completely definitional.
1995-05-13 nipkow 1995-05-13 Lambda calculus in de Bruijn notation. Proof of confluence.