src/Pure/Proof/extraction.ML
2007-05-31 ago simplified/unified list fold;
2007-05-10 ago Adapted to new naming scheme for definitions.
2007-05-07 ago simplified DataFun interfaces;
2007-04-26 ago renamed some old names Theory.xxx to Sign.xxx;
2007-04-20 ago adds extracted program to code theorem table
2007-04-16 ago canonical merge operations
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-13 ago canonical merge operations
2007-04-04 ago rep_thm/cterm/ctyp: removed obsolete sign field;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-12-15 ago avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-10-09 ago attribute: Context.mapping;
2006-10-04 ago insert replacing ins ins_int ins_string
2006-09-21 ago member (op =);
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-25 ago tuned;
2006-04-10 ago Term.itselfT;
2006-03-21 ago avoid polymorphic equality;
2006-02-06 ago Envir.(beta_)eta_contract;
2006-02-06 ago subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-02-03 ago canonical member/insert/merge;
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-11-16 ago tuned Pattern.match/unify;
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-06 ago introduced some new-style AList operations
2005-09-02 ago some 'assoc' etc. refactoring
2005-09-01 ago curried_lookup/update;
2005-08-31 ago refer to theory instead of low-level tsig;
2005-08-16 ago OuterKeyword;
2005-08-01 ago replaced atless by term_ord;
2005-07-15 ago tuned fold on terms;
2005-07-13 ago improved Net interface;
2005-07-13 ago (fix for an accidental commit)
2005-07-13 ago (intermediate commit)
2005-06-20 ago get_thm(s): Name;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-11 ago renamed Sign.intern_tycon to Sign.intern_type;
2005-06-09 ago can (Thm.get_axiom_i thy) name;
2005-06-05 ago Type.freeze;
2005-06-02 ago tuned;
2005-05-31 ago Theory.restore_naming;
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-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.
2005-01-24 ago Adapted to modified interface of PureThy.get_thm(s).
2004-12-10 ago Added term cache to function condrew in order to speed up rewriting.
2004-06-21 ago Merged in license change from Isabelle2004
2004-06-01 ago removed obsolete sort 'logic';
2004-03-19 ago Removing the datatype declaration of "order" allows the standard General.order
2003-01-29 ago Fixed bug in function corr.
2002-11-27 ago Correctness proofs are now modular, too.
2002-11-17 ago Fixed small bug that caused some definitions to be "forgotten".
2002-11-13 ago - exported functions etype_of and mk_typ
2002-09-30 ago Added check for axioms with "realizes Null A = A".