doc-src/IsarImplementation/checkglossary

- Now imports Code_Setup, rather than Set and Fun, since the theorems
about orderings are already needed in Set
- Moved "Dense orders" section to Set, since it requires set notation.
- The "Order on sets" section is no longer necessary, since it is subsumed by
the order on functions and booleans.
- Moved proofs of Least_mono and Least_equality to Set, since they require
set notation.
- In proof of "instance fun :: (type, order) order", use ext instead of
expand_fun_eq, since the latter is not yet available.
- predicate1I is no longer declared as introduction rule, since it interferes
with subsetI

#!/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";
    }
}