src/Pure/codegen.ML
2007-10-01 wenzelm 2007-10-01 auto_quickcheck: pervasive options, turned time_limit into plain int, simplified exception handling;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-09-24 wenzelm 2007-09-24 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
2007-09-20 berghofe 2007-09-20 - eval_term no longer computes result during compile time - generated ML code is now compiled via ML_Context.use_mltext rather than use_text; this makes sure that antiquotations are expanded - quickcheck now checks whether types to be substituted for type variables have correct sorts; this avoids spurious counterexamples - execution time for auto_quickcheck is now limited
2007-09-18 wenzelm 2007-09-18 simplified PrintMode interfaces;
2007-09-15 haftmann 2007-09-15 tuned
2007-09-10 berghofe 2007-09-10 Auto quickcheck now displays counterexample using Proof.goal_message rather than producing an error message.
2007-09-01 wenzelm 2007-09-01 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
2007-08-29 berghofe 2007-08-29 Deleted unused fillin_mixfix function.
2007-08-28 berghofe 2007-08-28 - restored old setup - new infrastructure for auto quickcheck - fixed bug in eta_expand that caused argument types to get mixed up
2007-08-16 haftmann 2007-08-16 fixed codegen setup
2007-08-15 haftmann 2007-08-15 updated code generator setup
2007-08-10 haftmann 2007-08-10 new structure for code generator modules
2007-08-07 haftmann 2007-08-07 new nbe implementation
2007-07-28 wenzelm 2007-07-28 tuned;
2007-07-23 wenzelm 2007-07-23 PrintMode.with_default;
2007-07-11 wenzelm 2007-07-11 Symbol.not_eof/sync is superceded by Symbol.is_regular (rules out further control symbols);
2007-07-08 wenzelm 2007-07-08 replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-10 haftmann 2007-05-10 consts in consts_code Isar commands are now referred to by usual term syntax
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-05-06 haftmann 2007-05-06 changed code generator invocation syntax
2007-04-20 haftmann 2007-04-20 unfold attribute now also accepts HOL equations
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; avoid rep_theory;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-01-21 wenzelm 2007-01-21 use_text: added name argument;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-13 haftmann 2006-12-13 cleanup
2006-12-09 wenzelm 2006-12-09 ML_Syntax.reserved(_names);
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-11-23 wenzelm 2006-11-23 moved ML syntax operations to structure ML_Syntax;
2006-10-23 haftmann 2006-10-23 switched merge_alists'' to AList.merge'' whenever appropriate
2006-10-20 haftmann 2006-10-20 Symtab.foldl replaced by Symtab.fold
2006-10-12 wenzelm 2006-10-12 print_evaluated_term: Toplevel.context_of;
2006-10-09 wenzelm 2006-10-09 moved Context.ml_output to Output.ml_output;
2006-09-21 wenzelm 2006-09-21 member (op =); ThmDatabase.is_ml_reserved; tuned oracle name;
2006-09-19 haftmann 2006-09-19 moved base setup for evaluation oracle hier
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-08-02 wenzelm 2006-08-02 removed obsolete Drule.frees/vars_of etc.;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-26 wenzelm 2006-04-26 tuned;
2006-04-13 wenzelm 2006-04-13 ignore sorts of consts declarations;
2006-04-06 haftmann 2006-04-06 added definitional code generator module: codegen_theorems.ML
2006-03-21 wenzelm 2006-03-21 remove (op =);
2006-02-22 haftmann 2006-02-22 abandoned merge_alists' in favour of generic AList.merge
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-08 haftmann 2006-02-08 introduced gen_distinct in place of distinct
2006-01-26 berghofe 2006-01-26 Fixed bug in code generator for primitive definitions that caused dependencies to get mixed up.
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-17 haftmann 2006-01-17 substantial improvements in code generator
2006-01-14 wenzelm 2006-01-14 generated code: raise Match instead of ERROR;
2006-01-13 wenzelm 2006-01-13 removed obsolete sign_of;
2005-12-01 berghofe 2005-12-01 assoc_consts and assoc_types now check number of arguments in template.
2005-11-29 haftmann 2005-11-29 exported customized syntax interface
2005-11-07 haftmann 2005-11-07 added proper fillin_mixfix
2005-11-07 haftmann 2005-11-07 added fillin_mixfix, replace_quote