1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-12-03 paulson 1997-12-03 Miniscoping now used except for one proof
1997-10-20 wenzelm 1997-10-20 adapted to qualified names;
1997-10-10 wenzelm 1997-10-10 fixed dots;
1996-09-09 paulson 1996-09-09 These simpsets must not use miniscoping
1996-01-29 clasohm 1996-01-29 expanded tabs
1995-05-03 clasohm 1995-05-03 replaced store_thm by bind_thm
1994-11-30 clasohm 1994-11-30 added qed and qed_goal[w]
1994-10-19 lcp 1994-10-19 CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification CCL/CCL, Fix, Gfp, Hered, Set, Term, Trancl, Type, Wfd: expanded shorthands
1994-09-14 wenzelm 1994-09-14 now uses Sign.const_type;
1994-03-17 lcp 1994-03-17 CCL/ccl.ML/po_refl_iff_T: deleted reference to make_iff_T CCL/ccl.ML/CCL_ss: now includes po_refl RS P_iff_T
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