src/Pure/Proof/extraction.ML
2007-10-06 wenzelm 2007-10-06 simplified interfaces for outer syntax;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-10 berghofe 2007-05-10 Adapted to new naming scheme for definitions.
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-26 wenzelm 2007-04-26 renamed some old names Theory.xxx to Sign.xxx;
2007-04-20 haftmann 2007-04-20 adds extracted program to code theorem table
2007-04-16 haftmann 2007-04-16 canonical merge operations
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-13 haftmann 2007-04-13 canonical merge operations
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping;
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-25 wenzelm 2006-04-25 tuned;
2006-04-10 wenzelm 2006-04-10 Term.itselfT;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract; TableFun: renamed xxx_multi to xxx_list;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2006-02-03 wenzelm 2006-02-03 canonical member/insert/merge;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-11-16 wenzelm 2005-11-16 tuned Pattern.match/unify;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-06 haftmann 2005-09-06 introduced some new-style AList operations
2005-09-02 haftmann 2005-09-02 some 'assoc' etc. refactoring
2005-09-01 wenzelm 2005-09-01 curried_lookup/update; tuned;
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-08-01 wenzelm 2005-08-01 replaced atless by term_ord;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms; tuned assoc;
2005-07-13 wenzelm 2005-07-13 improved Net interface;
2005-07-13 haftmann 2005-07-13 (fix for an accidental commit)
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-11 wenzelm 2005-06-11 renamed Sign.intern_tycon to Sign.intern_type;
2005-06-09 wenzelm 2005-06-09 can (Thm.get_axiom_i thy) name; removed duplicate code;
2005-06-05 wenzelm 2005-06-05 Type.freeze;
2005-06-02 wenzelm 2005-06-02 tuned;
2005-05-31 wenzelm 2005-05-31 Theory.restore_naming; tuned fold;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-21 berghofe 2005-04-21 Adapted to new interface of instantiation and unification / matching functions.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-12-10 berghofe 2004-12-10 Added term cache to function condrew in order to speed up rewriting.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-03-19 paulson 2004-03-19 Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.