src/Pure/ROOT.ML
2009-10-01 wenzelm 2009-10-01 Concurrently cached values.
2009-10-01 wenzelm 2009-10-01 more official status of sequential implementations; tuned;
2009-10-01 wenzelm 2009-10-01 separate concurrent/sequential versions of lazy evaluation; lazy based on future avoids wasted evaluations;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-28 wenzelm 2009-09-28 Dummy version of state variables -- plain refs for sequential access.
2009-08-11 wenzelm 2009-08-11 clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
2009-07-25 wenzelm 2009-07-25 renamed structure Display_Goal to Goal_Display;
2009-07-24 wenzelm 2009-07-24 renamed Pure/tctical.ML to Pure/tactical.ML;
2009-07-20 wenzelm 2009-07-20 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display;
2009-07-16 wenzelm 2009-07-16 Support for copy-avoiding functions on pure values, at the cost of readability.
2009-06-06 wenzelm 2009-06-06 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
2009-06-04 wenzelm 2009-06-04 just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
2009-06-02 wenzelm 2009-06-02 early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap; late setup of ML_Env and ML_Compiler;
2009-06-01 wenzelm 2009-06-01 added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);
2009-06-01 wenzelm 2009-06-01 slightly later setup of ML and secure operations;
2009-04-01 wenzelm 2009-04-01 tuned comments;
2009-03-22 wenzelm 2009-03-22 ML/ml_test.ML: test of advanced ML compiler invocation in Poly/ML 5.3;
2009-03-17 wenzelm 2009-03-17 turned structure NetRules into general Item_Net, which is loaded earlier;
2009-02-28 wenzelm 2009-02-28 moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-31 wenzelm 2008-12-31 added old_term.ML;
2008-12-15 haftmann 2008-12-15 moved value.ML to src/Tools
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-09-29 wenzelm 2008-09-29 added context_position.ML;
2008-09-22 wenzelm 2008-09-22 removed deriv.ML which is now incorporated into thm.ML;
2008-09-18 wenzelm 2008-09-18 added deriv.ML: Abstract derivations based on raw proof terms.
2008-09-11 wenzelm 2008-09-11 separate Concurrent/ROOT.ML;
2008-09-08 wenzelm 2008-09-08 added Concurrent/task_queue.ML;
2008-09-07 wenzelm 2008-09-07 added Concurrent/future.ML;
2008-09-04 wenzelm 2008-09-04 added Concurrent/mailbox.ML;
2008-09-04 wenzelm 2008-09-04 added Concurrent/schedule.ML;
2008-07-17 wenzelm 2008-07-17 structure Distribution: swapped default for is_official;
2008-07-11 haftmann 2008-07-11 tuned order
2008-06-18 wenzelm 2008-06-18 load type_infer.ML after Syntax module;
2008-06-18 wenzelm 2008-06-18 load proof term operations later;
2008-04-12 wenzelm 2008-04-12 removed obsolete compress.ML
2008-03-15 wenzelm 2008-03-15 removed obsolete fact_index.ML; added facts.ML;
2008-02-25 wenzelm 2008-02-25 tuned structure Distribution;
2008-02-21 wenzelm 2008-02-21 more elaborate structure Distribution (filled-in by makedist);
2008-01-24 wenzelm 2008-01-24 removed obsolete context_position.ML (superseded by Position.thread_data);
2007-12-31 wenzelm 2007-12-31 removed obsolete banner;
2007-11-28 wenzelm 2007-11-28 removed typedecl.ML (cf. object_logic.ML);
2007-11-23 haftmann 2007-11-23 separated typedecl module, providing typedecl command with interpretation
2007-10-11 wenzelm 2007-10-11 load axclass.ML before Isar;
2007-10-04 wenzelm 2007-10-04 load variable.ML before conv.ML;
2007-09-20 wenzelm 2007-09-20 added interpretation.ML;
2007-09-14 wenzelm 2007-09-14 moved ML_XXX.ML files to Pure/ML;
2007-08-28 berghofe 2007-08-28 codegen.ML is now loaded in Pure again.
2007-08-14 wenzelm 2007-08-14 tuned order;
2007-08-14 wenzelm 2007-08-14 use logic.ML earlier; added primitive_defs.ML;
2007-08-13 wenzelm 2007-08-13 added Syntax/simple_syntax.ML;
2007-08-01 wenzelm 2007-08-01 renamed config_option.ML to config.ML;
2007-07-28 wenzelm 2007-07-28 use config_option.ML after sign.ML;
2007-07-27 wenzelm 2007-07-27 renamed config.ML to config_option.ML;
2007-07-25 wenzelm 2007-07-25 added config.ML;
2007-07-17 wenzelm 2007-07-17 simplified loading of ML files -- no static forward references;
2007-07-10 wenzelm 2007-07-10 use position.ML earlier;
2007-07-09 wenzelm 2007-07-09 use position.ML after pretty.ML;
2007-06-13 wenzelm 2007-06-13 added context_position.ML;