--- 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"
--- 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 =
--- 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 =
--- 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 =