# HG changeset patch
# User wenzelm
# Date 1368361516 -7200
# Node ID 958d439b3013fc6244bffe8e5eadb99f9ea0d398
# Parent  65548ab2fc558b26cd3be37dfe07b5751b2fd1a5
decentralized historic settings;

diff -r 65548ab2fc55 -r 958d439b3013 etc/settings
--- a/etc/settings	Sun May 12 13:56:21 2013 +0200
+++ b/etc/settings	Sun May 12 14:25:16 2013 +0200
@@ -142,36 +142,6 @@
 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
 #SMLNJ_CYGWIN_RUNTIME=1
 
-## Set HOME only for tools you have installed!
-
-# SVC (Stanford Validity Checker)
-#SVC_HOME=
-#SVC_MACHINE=i386-redhat-linux
-#SVC_MACHINE=sparc-sun-solaris
-
-# MiniSat 1.14 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
-#MINISAT_HOME=/usr/local/bin
-
-# zChaff (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
-#ZCHAFF_HOME=/usr/local/bin
-
-# BerkMin561 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
-#BERKMIN_HOME=/usr/local/bin
-#BERKMIN_EXE=BerkMin561-linux
-#BERKMIN_EXE=BerkMin561-solaris
-
-# Jerusat 1.3 (SAT Solver, cf. src/HOL/Tools/sat_solver.ML)
-#JERUSAT_HOME=/usr/local/bin
-
-# 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=CPLEX
-#CPLEX_PATH=cplex
-# Second option: use the open source glpk solver
-#LP_SOLVER=GLPK
-#GLPK_PATH=glpsol
-
 # Misc programming languages
 #ISABELLE_GHC="/usr/bin/ghc"
 #ISABELLE_OCAML="/usr/bin/ocaml"
diff -r 65548ab2fc55 -r 958d439b3013 src/HOL/Matrix_LP/Cplex_tools.ML
--- a/src/HOL/Matrix_LP/Cplex_tools.ML	Sun May 12 13:56:21 2013 +0200
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Sun May 12 14:25:16 2013 +0200
@@ -1,5 +1,15 @@
 (*  Title:      HOL/Matrix_LP/Cplex_tools.ML
     Author:     Steven Obua
+
+Relevant Isabelle environment settings:
+
+  # 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=CPLEX
+  #CPLEX_PATH=cplex
+  # Second option: use the open source glpk solver
+  #LP_SOLVER=GLPK
+  #GLPK_PATH=glpsol
 *)
 
 signature CPLEX =
diff -r 65548ab2fc55 -r 958d439b3013 src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Sun May 12 13:56:21 2013 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sun May 12 14:25:16 2013 +0200
@@ -3,6 +3,22 @@
     Copyright   2004-2009
 
 Interface to external SAT solvers, and (simple) built-in SAT solvers.
+
+Relevant Isabelle environment settings:
+
+  # MiniSat 1.14
+  #MINISAT_HOME=/usr/local/bin
+
+  # zChaff
+  #ZCHAFF_HOME=/usr/local/bin
+
+  # BerkMin561
+  #BERKMIN_HOME=/usr/local/bin
+  #BERKMIN_EXE=BerkMin561-linux
+  #BERKMIN_EXE=BerkMin561-solaris
+
+  # Jerusat 1.3
+  #JERUSAT_HOME=/usr/local/bin
 *)
 
 signature SAT_SOLVER =
diff -r 65548ab2fc55 -r 958d439b3013 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Sun May 12 13:56:21 2013 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Sun May 12 14:25:16 2013 +0200
@@ -14,6 +14,12 @@
   in either operand.
 
 For each variable of type nat, an assumption is added that it is non-negative.
+
+Relevant Isabelle environment settings:
+
+  #SVC_HOME=
+  #SVC_MACHINE=i386-redhat-linux
+  #SVC_MACHINE=sparc-sun-solaris
 *)
 
 structure Svc =