src/Tools/nbe.ML
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-19 haftmann 2010-05-19 new version of triv_of_class machinery without legacy_unconstrain
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-05-09 wenzelm 2010-05-09 reactivated Thm.legacy_unconstrainT for Nbe.lift_triv_classes_conv;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-02 haftmann 2010-03-02 dropped superfluous naming
2010-02-24 haftmann 2010-02-24 tuned whitespace
2010-01-04 haftmann 2010-01-04 code cache only persists on equal theories
2010-01-04 haftmann 2010-01-04 code cache without copy; tuned
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-09 haftmann 2009-09-09 moved eq handling in nbe into separate oracle
2009-07-21 haftmann 2009-07-21 integrated add_triv_classes into evaluation stack
2009-07-08 haftmann 2009-07-08 tuned structure Code internally
2009-07-07 haftmann 2009-07-07 tuned interface of structure Code
2009-06-30 haftmann 2009-06-30 all variable names are optional
2009-06-30 haftmann 2009-06-30 variable names in abstractions are optional
2009-06-19 haftmann 2009-06-19 more appropriate syntax for IML abstraction
2009-05-14 haftmann 2009-05-14 merged module code_unit.ML into code.ML
2009-05-07 haftmann 2009-05-07 treat frees driectly by the LCF kernel
2009-05-06 haftmann 2009-05-06 explicit type arguments in constants
2009-04-24 haftmann 2009-04-24 generic postprocessing scheme for term evaluations
2009-04-17 haftmann 2009-04-17 re-engineering of evaluation conversions
2009-04-17 haftmann 2009-04-17 diagnostic commands now in code_thingol; tuned code of funny continuations
2009-03-23 wenzelm 2009-03-23 more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
2009-03-05 wenzelm 2009-03-05 Thm.add_oracle interface: replaced old bstring by binding;
2009-02-20 haftmann 2009-02-20 maintain order of constructors in datatypes; clarified conventions for type schemes
2008-12-31 wenzelm 2008-12-31 use regular Term.add_XXX etc.;
2008-10-28 haftmann 2008-10-28 restored incremental code generation
2008-10-22 haftmann 2008-10-22 code identifier namings are no longer imperative
2008-09-30 haftmann 2008-09-30 clarified codegen interfaces
2008-09-25 haftmann 2008-09-25 non left-linear equations for nbe
2008-09-23 haftmann 2008-09-23 case default fallback for NBE
2008-09-19 haftmann 2008-09-19 made SMLNJ happy
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-09-17 wenzelm 2008-09-17 ML_Context.evaluate: proper context (for ML environment);
2008-09-16 haftmann 2008-09-16 generic value command
2008-08-28 haftmann 2008-08-28 restructured and split code serializer module
2008-07-15 haftmann 2008-07-15 tuned code theorem bookkeeping
2008-07-08 haftmann 2008-07-08 clarified code
2008-06-18 wenzelm 2008-06-18 simplified TypeInfer.infer_types;
2008-06-10 haftmann 2008-06-10 major refactorings in code generator modules
2008-05-23 haftmann 2008-05-23 explicit type schemes for functions
2008-05-18 wenzelm 2008-05-18 command 'normal_form': proper context via Variable.auto_fixes;
2008-05-17 wenzelm 2008-05-17 cat_lines;
2008-04-24 haftmann 2008-04-24 moved 'trivial classes' to foundation of code generator
2008-04-22 haftmann 2008-04-22 different handling of eq class for nbe
2008-02-13 haftmann 2008-02-13 using integers for pattern matching
2008-01-29 haftmann 2008-01-29 cleaned up evaluation interfaces
2008-01-22 haftmann 2008-01-22 tuned
2008-01-21 haftmann 2008-01-21 tuned
2008-01-18 haftmann 2008-01-18 improved implementation
2008-01-08 haftmann 2008-01-08 tuned comment