doc-src/IsarImplementation/checkglossary

tuned the proof

#!/usr/bin/env perl
# $Id$

use strict;

my %defs = ();
my %refs = ();

while (<ARGV>) {
    if (m,\\glossaryentry\{\w*\\bf *((\w|\s)+)@,) {
	$defs{lc $1} = 1;
    }
    while (m,\\seeglossary *\{((\w|\s)+)\},g) {
	$refs{lc $1} = 1;
    }
}

print "Glossary definitions:\n";
foreach (sort(keys(%defs))) {
    print "  \"$_\"\n";
}

foreach (keys(%refs)) {
    s,s$,,;
    if (!defined($defs{$_})) {
	print "### Undefined glossary reference: \"$_\"\n";
    }
}