lib/Tools/convert

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: David von Oheimb, TU Muenchen
#
# DESCRIPTION: convert legacy tactic scripts to Isabelle/Isar tactic emulation


## diagnostics

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

function usage()
{
  echo
  echo "Usage: $PRG [FILES|DIRS...]"
  echo
  echo "  Recursively find .ML files, converting legacy tactic scripts to"
  echo "  Isabelle/Isar tactic emulation."
  echo "  Note: conversion is only approximated, based on some heuristics."
  echo
  echo "  Renames old versions of FILES by appending \"~0~\"."
  echo "  Creates new versions of FILES by appending \".thy\"."
  echo
  exit 1
}


## process command line

[ "$#" -eq 0 -o "$1" = "-?" ] && usage

SPECS="$@"; shift "$#"


## main

#set by configure
AUTO_PERL=perl

find $SPECS \( -name \*.ML \) -print | \
  xargs "$AUTO_PERL" -w "$ISABELLE_HOME/lib/scripts/convert.pl"