1.1 --- a/etc/settings Thu Mar 06 19:21:22 2008 +0100
1.2 +++ b/etc/settings Thu Mar 06 19:21:23 2008 +0100
1.3 @@ -138,14 +138,8 @@
1.4 ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
1.5
1.6 # Heap output location. ML system identifier is appended automatically later on.
1.7 -if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
1.8 - #Isabelle build tells us to store heaps etc. within the distribution.
1.9 - ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
1.10 - ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
1.11 -else
1.12 - ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
1.13 - ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
1.14 -fi
1.15 +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
1.16 +ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
1.17
1.18 # Site settings check -- just to make it a little bit harder to copy this file verbatim!
1.19 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
1.20 @@ -220,8 +214,13 @@
1.21
1.22 ## Set HOME only for tools you have installed!
1.23
1.24 +# External provers
1.25 +E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
1.26 +VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "")
1.27 +SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")
1.28 +
1.29 # HOL4 proof objects (cf. Isabelle/src/HOL/Import)
1.30 -HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
1.31 +#HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
1.32
1.33 # SVC (Stanford Validity Checker)
1.34 #SVC_HOME=
1.35 @@ -258,8 +257,3 @@
1.36 # Second option: use the open source glpk solver
1.37 #LP_SOLVER=GLPK
1.38 #GLPK_PATH=glpsol
1.39 -
1.40 -# External provers
1.41 -E_HOME=$(choosefrom "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" "/usr/local/E" "")
1.42 -VAMPIRE_HOME=$(choosefrom "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" "/usr/local/Vampire" "")
1.43 -SPASS_HOME=$(choosefrom "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" "/usr/local/SPASS" "")