1997-12-03 paulson 1997-12-03 Miniscoping now used except for one proof
1997-10-10 wenzelm 1997-10-10 fixed dots;
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-09-09 paulson 1996-09-09 These simpsets must not use miniscoping
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