src/HOL/Tools/rewrite_hol_proof.ML
Wed, 23 Apr 2003 00:12:14 +0200 berghofe elim_cong now eta-expands proofs on the fly if required.
Mon, 30 Sep 2002 16:27:38 +0200 berghofe - additional congruence rules for boolean operators
Sun, 21 Jul 2002 15:43:14 +0200 berghofe Rules for rewriting HOL proofs.
less more (0) tip