2007-08-29 ago Deleted unused fillin_mixfix function.
2007-08-28 ago - restored old setup
2007-08-16 ago fixed codegen setup
2007-08-15 ago updated code generator setup
2007-08-10 ago new structure for code generator modules
2007-08-07 ago new nbe implementation
2007-07-28 ago tuned;
2007-07-23 ago PrintMode.with_default;
2007-07-11 ago Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-08 ago replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-05-31 ago simplified/unified list fold;
2007-05-10 ago consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-07 ago simplified DataFun interfaces;
2007-05-06 ago changed code generator invocation syntax
2007-04-20 ago unfold attribute now also accepts HOL equations
2007-04-14 ago cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 ago rep_thm/cterm/ctyp: removed obsolete sign field;
2007-01-21 ago use_text: added name argument;
2006-12-15 ago avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-13 ago cleanup
2006-12-09 ago ML_Syntax.reserved(_names);
2006-11-23 ago prefer Proof.context over Context.generic;
2006-11-23 ago moved ML syntax operations to structure ML_Syntax;
2006-10-23 ago switched merge_alists'' to AList.merge'' whenever appropriate
2006-10-20 ago Symtab.foldl replaced by Symtab.fold
2006-10-12 ago print_evaluated_term: Toplevel.context_of;
2006-10-09 ago moved Context.ml_output to Output.ml_output;
2006-09-21 ago member (op =);
2006-09-19 ago moved base setup for evaluation oracle hier
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-08-02 ago removed obsolete Drule.frees/vars_of etc.;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-06-07 ago renamed Type.(un)varifyT to Logic.(un)varifyT;
2006-04-29 ago tuned;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-26 ago tuned;
2006-04-13 ago ignore sorts of consts declarations;
2006-04-06 ago added definitional code generator module: codegen_theorems.ML
2006-03-21 ago remove (op =);
2006-02-22 ago abandoned merge_alists' in favour of generic AList.merge
2006-02-15 ago removed distinct, renamed gen_distinct to distinct;
2006-02-08 ago introduced gen_distinct in place of distinct
2006-01-26 ago Fixed bug in code generator for primitive definitions that
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-17 ago substantial improvements in code generator
2006-01-14 ago generated code: raise Match instead of ERROR;
2006-01-13 ago removed obsolete sign_of;
2005-12-01 ago assoc_consts and assoc_types now check number of arguments in template.
2005-11-29 ago exported customized syntax interface
2005-11-07 ago added proper fillin_mixfix
2005-11-07 ago added fillin_mixfix, replace_quote
2005-11-07 ago added fillin_mixfix' needed by serializer
2005-09-27 ago Optimized unfold_attr.
2005-09-25 ago Fixed print mode problem in test_term.
2005-09-21 ago - Added eval_term function and value command
2005-09-20 ago introduced AList module in favor of assoc etc.
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-05 ago curried_lookup/update;
2005-08-25 ago Implemented incremental code generation.