src/HOL/Lambda/Eta.ML
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1996-11-04 nipkow 1996-11-04 Used nat_trans_tac. New Eta. various smaller changes.
1996-10-21 nipkow 1996-10-21 Used trans_tac (see Provers/nat_transitive.ML) to automate arithmetic.
1996-10-10 paulson 1996-10-10 Tidied some proofs: changed needed for de Morgan laws
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-08-19 paulson 1996-08-19 Tidied some proofs, maybe using less_SucE
1996-05-22 nipkow 1996-05-22 Added comparison with implicit rule Fun(lift s 0 @ Var 0) -e> s
1996-05-07 paulson 1996-05-07 Updated for new form of induction rules
1996-04-23 oheimb 1996-04-23 repaired critical proofs depending on the order inside non-confluent SimpSets
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-25 nipkow 1995-10-25 Moved some thms to Arith and to Trancl.
1995-10-06 nipkow 1995-10-06 New version with eta reduction.