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

--- a/etc/settings	Mon Aug 01 11:24:19 2005 +0200
+++ b/etc/settings	Mon Aug 01 11:39:33 2005 +0200
@@ -219,9 +219,13 @@
 HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
 
 # For configuring HOL/Matrix/cplex
+# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
 # First option: use the commercial cplex solver
-#LP_SOLVER_NAME=CPLEX
-#LP_SOLVER_PATH=cplex
+# LP_SOLVER=CPLEX
+# CPLEX_PATH=cplex
 # Second option: use the open source glpk solver
-#LP_SOLVER_NAME=GLPK
-#LP_SOLVER_PATH=glpsol
+# LP_SOLVER=GLPK
+# GLPK_PATH=glpsol
+
+# toogles the detail of the error message in case of a cyclic definition
+DEFS_CHAIN_HISTORY=ON

--- a/src/HOL/Library/Library.thy	Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Library/Library.thy	Mon Aug 01 11:39:33 2005 +0200
@@ -17,9 +17,7 @@
   While_Combinator
   Word
   Zorn
-  (*List_Prefix*)
   Char_ord
-  List_lexord
 begin
 end
 (*>*)

--- a/src/HOL/Library/Library/ROOT.ML	Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Library/Library/ROOT.ML	Mon Aug 01 11:39:33 2005 +0200
@@ -1,1 +1,3 @@
 use_thy "Library";
+use_thy "List_Prefix";
+use_thy "List_lexord";

--- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Mon Aug 01 11:39:33 2005 +0200
@@ -35,6 +35,8 @@
 			 | Optimal of string * 
 				      (((* name *) string * 
 					(* value *) string) list)
+
+    datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
 						     
     exception Load_cplexFile of string
     exception Load_cplexResult of string
@@ -51,12 +53,20 @@
 
     val is_normed_cplexProg : cplexProg -> bool
 
+    val get_solver : unit -> cplexSolver
+    val set_solver : cplexSolver -> unit
     val solve : cplexProg -> cplexResult
 end;
 
 structure Cplex  : CPLEX =
 struct
 
+datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
+
+val cplexsolver = ref SOLVER_DEFAULT;
+fun get_solver () = !cplexsolver;
+fun set_solver s = (cplexsolver := s);
+
 exception Load_cplexFile of string;
 exception Load_cplexResult of string;
 exception Save_cplexFile of string;
@@ -1139,7 +1149,7 @@
 	val lpname = tmp_file (name^".lp")
 	val resultname = tmp_file (name^".txt")
 	val _ = save_cplexFile lpname prog		
-	val cplex_path = getenv "LP_SOLVER_PATH"
+	val cplex_path = getenv "GLPK_PATH"
 	val cplex = if cplex_path = "" then "glpsol" else cplex_path
 	val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
 	val answer = execute command
@@ -1171,7 +1181,7 @@
 	val resultname = tmp_file (name^".txt")
 	val scriptname = tmp_file (name^".script")
 	val _ = save_cplexFile lpname prog		
-	val cplex_path = getenv "LP_SOLVER_PATH"
+	val cplex_path = getenv "CPLEX_PATH"
 	val cplex = if cplex_path = "" then "cplex" else cplex_path
 	val _ = write_script scriptname lpname resultname
 	val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
@@ -1188,10 +1198,14 @@
     end
 
 fun solve prog = 
-    case getenv "LP_SOLVER_NAME" of
-	"CPLEX" => solve_cplex prog
-      | "GLPK" => solve_glpk prog
-      | _ => raise (Execute ("LP_SOLVER_NAME must be set to CPLEX or to GLPK"));
+    case get_solver () of
+      SOLVER_DEFAULT => 
+        (case getenv "LP_SOLVER" of
+	   "CPLEX" => solve_cplex prog
+         | "GLPK" => solve_glpk prog
+         | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
+    | SOLVER_CPLEX => solve_cplex prog
+    | SOLVER_GLPK => solve_glpk prog
 		   
 end;