2008-04-22 haftmann 2008-04-22 added theory Sublist_Order
2007-11-06 wenzelm 2007-11-06 removed dependencies on Size_Change_Termination from HOL-Library;
2007-07-31 wenzelm 2007-07-31 simultaneous use_thys;
2007-02-26 krauss 2007-02-26 Added formalization of size-change principle (experimental).
2006-10-01 wenzelm 2006-10-01 tuned;
2005-08-01 obua 2005-08-01 1. changed configuration variables for linear programming (Cplex_tools): LP_SOLVER is either CPLEX or GLPK CPLEX_PATH is the path to the cplex binary GLPK_PATH is the path to the glpk binary The change makes it possible to switch between glpk and cplex at runtime. 2. moved conflicting list theories out of Library.thy into ROOT.ML
2001-07-03 wenzelm 2001-07-03 Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential uses of this ML file (HOL/Library is in the default load path);