2002-01-12 ago renamed forall_elim_vars_safe to gen_all;
2002-01-11 ago replace gen_all by forall_elim_vars_safe;
2002-01-03 ago Some new theorems for ordinals
2000-09-07 ago tuned ML code (the_context, bind_thms(s));
2000-06-30 ago removal of batch-style proofs
2000-06-28 ago tidying and unbatchifying
1999-01-13 ago datatype package improvements
1999-01-12 ago eliminated global/local names;
1998-09-24 ago renamed mk_meta_eq to mk_eq
1998-09-22 ago tidying
1997-11-03 ago isatool fixclasimp;
1997-10-10 ago fixed dots;
1997-01-03 ago Implicit simpsets and clasets for FOL and ZF