1996-01-29 clasohm 1996-01-29 expanded tabs
1994-11-30 clasohm 1994-11-30 added qed and qed_goal[w]
1993-09-20 lcp 1993-09-20 Installation of new simplfier. Previously appeared to set up the old simplifier to rewrite with the partial ordering [=, something not possible with the new simplifier. But such rewriting appears not to have actually been used, and there were few complications. In terms.ML setloop was used to avoid infinite rewriting with the letrec rule. Congruence rules were deleted, and an occasional SIMP_TAC had to become asm_simp_tac.
1993-09-16 clasohm 1993-09-16 Initial revision