2009-03-12 ago tuned;
2009-03-12 ago renamed assms_of to all_assms_of, and prems_of to all_prems_of;
2009-01-21 ago eliminated obsolete var morphism;
2009-01-21 ago binding replaces bstring
2008-12-04 ago cleaned up binding module and related code
2008-03-28 ago Context.>> : operate on Context.generic;
2008-03-27 ago eliminated delayed theory setup
2008-03-25 ago setup for dynamic "prems" (legacy);
2007-05-07 ago simplified DataFun interfaces;
2006-12-06 ago export: added explicit term operation;
2006-11-30 ago qualified MetaSimplifier.norm_hhf(_protect);
2006-11-29 ago assms_of: cterm;
2006-11-24 ago added export_morphism;
2006-08-02 ago simplified export: no Seq.seq;
2006-07-27 ago Local assumptions, parameterized by export rules.