etc/settings

 ### External reasoning tools
 ###
 
 ## Set HOME only for tools you have installed!
 
+# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
+HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
+
 # SVC (Stanford Validity Checker)
 #SVC_HOME=
 #SVC_MACHINE=i386-redhat-linux
 #SVC_MACHINE=sparc-sun-solaris
 

 #BERKMIN_EXE=BerkMin561-linux
 #BERKMIN_EXE=BerkMin561-solaris
 
 # Jerusat 1.3 (SAT Solver)
 #JERUSAT_HOME=/usr/local/bin
-
-# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
-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=CPLEX