diff -r a3c7bd201da7 -r 9590972c2caf lib/Tools/yxml
--- a/lib/Tools/yxml	Sun Feb 28 21:19:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: simple XML to YXML converter
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG"
-  echo
-  echo "  Convert XML (stdin) to YXML (stdout)."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-exec "$ISABELLE_HOME/lib/scripts/yxml"