doc-src/IsarImplementation/makeglossary
author wenzelm
Fri, 27 Jan 2006 19:03:07 +0100
changeset 18801 b913ce69660c
parent 18537 2681f9e34390
permissions -rwxr-xr-x
moved theorem tags from Drule to PureThy; replaced kind attribute by kind string; tuned name_multi: index > 1 only; added note_thmss_qualified (from Isar/locale.ML);

#!/bin/sh
# $Id$

NAME="$1"
makeindex -s nomencl -o "${NAME}.gls" "${NAME}.glo"
./checkglossary "${NAME}.glo"