2012-02-15 ago renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2010-03-27 ago moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-11-02 ago modernized structure Simple_Syntax;
2009-10-28 ago proper binding;
2009-09-29 ago modernized Balanced_Tree;
2009-03-31 ago added dest_conjunctions (cf. Logic.dest_conjunctions);
2009-01-21 ago removed Ids;
2008-11-20 ago Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
2008-10-23 ago renamed Thm.get_axiom_i to Thm.axiom;
2008-04-15 ago Thm.forall_elim_var(s);
2008-03-29 ago certify wrt. dynamic context;
2008-03-27 ago eliminated theory ProtoPure;
2007-10-11 ago moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
2007-08-13 ago SimpleSyntax.read_prop;
2007-07-03 ago removed obsolete mk_conjunction_list, intr/elim_list;
2007-06-19 ago balanced conjunctions;
2006-11-28 ago simplified '?' operator;
2006-09-21 ago Thm.dest_binop;
2006-09-12 ago intr/elim: use constant complexity thanks to tuned Thm.instantiate/implies_elim;
2006-07-30 ago Thm.adjust_maxidx;
2006-07-29 ago added mk_conjunction_list;
2006-07-27 ago eliminated obsolete freeze_thaw;
2006-04-13 ago Meta-level conjunction.