lib/scripts/isabelle-platform

fixed detection of tautologies -- things like "a = b" in a structured proof, where a and b are Frees, shouldn't be discarted as tautologies

# -*- shell-script -*- :mode=shellscript:
#
# determine general hardware and operating system type for Isabelle
#
# NOTE: The ML system or JVM may have their own idea about the platform!

ISABELLE_PLATFORM32=""
ISABELLE_PLATFORM64=""

case $(uname -s) in
  Linux)
    case $(uname -m) in
      i?86)
        ISABELLE_PLATFORM32=x86-linux
        ;;
      x86_64)
        ISABELLE_PLATFORM32=x86-linux
        ISABELLE_PLATFORM64=x86_64-linux
        ;;
    esac
    ;;
  Darwin)
    case $(uname -m) in
      i?86)
        ISABELLE_PLATFORM32=x86-darwin
        if [ "$(sysctl -n hw.optional.x86_64 2>/dev/null)" = 1 ]; then
          ISABELLE_PLATFORM64=x86_64-darwin
        fi
        ;;
      x86_64)
        ISABELLE_PLATFORM32=x86-darwin
        ISABELLE_PLATFORM64=x86_64-darwin
        ;;
    esac
    ;;
  CYGWIN_NT*)
    case $(uname -m) in
      i?86 | x86_64)
        ISABELLE_PLATFORM32=x86-cygwin
        ;;
    esac
    ;;
  *BSD)
    case $(uname -m) in
      i?86 | x86_64)
        ISABELLE_PLATFORM32=x86-linux  #cf. BSD Linux Binary Compatibility
        ;;
    esac
    ;;
esac

ISABELLE_PLATFORM="$ISABELLE_PLATFORM32"