doc-src/IsarImplementation/makeglossary
author wenzelm
Thu, 12 Jun 2008 22:29:51 +0200
changeset 27184 b1483d423512
parent 18537 2681f9e34390
permissions -rwxr-xr-x
export just one setup function; more antiquotations; to_nnf: import open, avoiding internal variables (bounds); ThmCache: added table of seen fact names; reorganized skolem_thm/skolem_fact/saturate_skolem_cache: maintain seen fact names, ensure idempotent operation for Theory.at_end; removed obsolete skolem attribute (NB: official fact name unavailable here);

#!/bin/sh
# $Id$

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