lib/Tools/makeall

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

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: apply make utility to all logics

## global settings

ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: $PRG [ARGS ...]"
  echo
  echo "  Apply isatool make to all logics (passing ARGS)."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

## main

[ "$1" = "-?" ] && usage

FAIL=""

echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"

for L in $ALL_LOGICS
do
  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || FAIL="$FAIL$L "
done

echo -n "Finished at "; date

ELAPSED=$("$ISABELLE_HOME/lib/scripts/showtime" "$SECONDS")
echo "$ELAPSED total elapsed time"

[ "$FAIL" = "" ] || fail "Logics ${FAIL}FAILED!"