2007-05-31 ago simplified/unified list fold;
2007-05-24 ago tuned Pure/General/name_space.ML
2007-05-07 ago simplified DataFun interfaces;
2007-04-04 ago tuned comment;
2007-01-20 ago ML tactic: proper context for compile and runtime;
2007-01-19 ago removed obsolete Method;
2007-01-19 ago adapted ML context operations;
2006-12-30 ago removed conditional combinator;
2006-12-18 ago switched argument order in *.syntax lifters
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-11-29 ago renamed SIMPLE_METHOD' to SIMPLE_METHOD'';
2006-11-29 ago COMP_INCR;
2006-08-03 ago moved bires_inst_tac etc. to rule_insts.ML;
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-12 ago removed duplicate of Tactic.make_elim_preserve;
2006-07-06 ago added method_i and Source_i;
2006-06-05 ago assm_tac: try rule termI;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-03-21 ago moved gen_eq_set to library.ML;
2006-03-04 ago text: added SelectGoals;
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-02-10 ago syntax: Context.generic;
2006-02-06 ago tuned;
2006-02-03 ago canonical member/insert/merge;
2006-01-31 ago (un)fold: removed '(raw)' option;
2006-01-29 ago method (un)folded: option '(raw)';
2006-01-28 ago (un)fold: support object-level rewrites;
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-10 ago generic attributes;
2005-12-22 ago conjunction_tac: single goal;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-11-30 ago method 'fact': SIMPLE_METHOD, i.e. insert facts;
2005-11-22 ago moved multi_resolve(s) to drule.ML;
2005-11-10 ago renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-28 ago added fact method;
2005-10-15 ago added primitive_text, succeed_text;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-22 ago renamed "rules" to "iprover"
2005-09-20 ago slight adaptions to library changes
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-13 ago added cheating, sorry_text (from skip_proofs.ML);
2005-09-08 ago introduces some modern-style AList operations
2005-09-01 ago curried_lookup/update;
2005-08-18 ago moved before proof.ML;
2005-07-19 ago Logic.incr_tvar;
2005-06-20 ago refl_tac: avoid failure of unification, i.e. confusing trace msg;
2005-06-17 ago (RAW_)METHOD_CASES: RuleCases.tactic;
2005-06-09 ago meths: NameSpace.table;
2005-05-31 ago renamed cond_extern to extern;
2005-05-17 ago tuned;
2005-04-23 ago removed structure PureIsar;
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
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.