1996-01-30 clasohm 1996-01-30 expanded tabs
1995-04-28 lcp 1995-04-28 Modified proofs for new claset primitives. The problem is that they enforce the "most recent added rule has priority" policy more strictly now.
1995-04-06 lcp 1995-04-06 Modified proofs for new hyp_subst_tac, and simplified them.
1995-02-27 lcp 1995-02-27 New example by Jacob Frost, tidied by lcp