- 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";
}
}