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);