uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
more robust handling of "|" within index;
# -*- shell-script -*-
#
# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
HOL_USEDIR_OPTIONS="-p 1"
ISABELLE_LOGIC=HOL