diff -r 2154f709fc25 -r 040b94ffbdde lib/Tools/yxml
--- a/lib/Tools/yxml	Sun Feb 28 15:34:50 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"