2006-10-13 ago Moved old inductive package to old_inductive_package.ML
2006-10-10 ago gen_rem(s) abandoned in favour of remove / subtract
2006-10-09 ago attribute: Context.mapping;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-06-07 ago renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-05-11 ago avoid raw equality on type thm;
2006-04-30 ago AxClass.axiomatize_arity_i;
2006-04-26 ago tuned;
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-02-06 ago Envir.(beta_)eta_contract;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2005-12-06 ago re-oriented some result tuples in PureThy
2005-12-01 ago oriented pairs theory * 'a to 'a * theory
2005-10-28 ago swapped add_datatype result
2005-10-21 ago OldGoals;
2005-09-19 ago introduced AList module
2005-09-12 ago introduced new-style AList operations
2005-07-15 ago tuned fold on terms;
2005-05-31 ago Theory.restore_naming;
2005-04-13 ago *** empty log message ***
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-08 ago add_dummies no longer uses transform_error but handles specific
2003-04-27 ago Fixed problem in add_elim_realizer (concerning inductive predicates with
2003-04-23 ago Fixed problem in add_elim_realizer which caused bound variables to
2002-11-27 ago Changed format of realizers / correctness proofs.
2002-11-13 ago New package for constructing realizers for introduction and elimination