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
* July 2005: Jeremy Avigad, Carnegie Mellon University
Various improvements of the HOL and HOL-Complex library.
* July 2005: Florian Haftmann, TUM
Some combinators for linear functional transformations in ML:
|-> #-> fold_map etc.
* July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM
Some structured proofs about completeness of real numbers.
* May 2005: Rafal Kolanski, NICTA
Substantially improved retrieval of facts from theory/proof context.
* May 2005: Florian Haftmann, TUM
Several new antiquotation.
* February 2005: Lucas Dixon, University of Edinburgh
Substantially improved subst method.
$Id$