2007-04-15 ago Thm.fold_terms;
2007-04-14 ago tuned signature;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-14 ago added trans_terms/props;
2006-12-12 ago tuned expand_term;
2006-12-07 ago reorganized structure Tactic vs. MetaSimplifier;
2006-12-07 ago expand_term: based on Envir.expand_term;
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-12-06 ago added expand;
2006-11-29 ago added export;
2006-11-28 ago simplified '?' operator;
2006-11-23 ago prefer Proof.context over Context.generic;
2006-10-11 ago add_defs: declare terms;
2006-10-09 ago simplified derived_def;
2006-10-07 ago replaced add_def by more elaborate add_defs;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-27 ago moved basic assumption operations from structure ProofContext to Assumption;
2006-07-08 ago Goal.prove: context;
2006-07-06 ago def_export: Drule.generalize;
2006-06-15 ago ProofContext: moved variable operations to struct Variable;
2006-05-07 ago removed 'concl is' patterns;
2006-02-06 ago cert_def: use Logic.dest_def;
2006-02-02 ago tuned comments;
2006-01-31 ago (un)fold: no raw flag;
2006-01-31 ago export meta_rewrite_rule;
2006-01-29 ago added attributes defn_add/del;
2006-01-28 ago Basic operations on local definitions.
2001-10-16 ago simplified exporter interface;
2001-10-10 ago Removed unnecessary application of Drule.standard.
2000-11-13 ago tuned statement args;
2000-07-30 ago local_def(_i): no constraint on var;
2000-07-13 ago use ProofContext.bind_skolem;
2000-07-13 ago prep rhs in original context;
2000-05-05 ago GPLed;
2000-01-05 ago prepare patterns only once;
1999-09-30 ago local_def_i: typ option;
1999-09-07 ago tuned;
1999-09-01 ago Thm.def_name;
1999-08-18 ago assume: multiple args;
1999-07-13 ago handle cgoal;
1999-07-09 ago added Isar/local_defs.ML;