All subgoals sent to the watcher at once now. Rules added to parser for Spass proofs. If parsing or translation fails on a proof, the Spass proof is printed out in PG.

added Isar_examples/Drinker.thy;

full Display.pprint_theory for ML toplevel facilitates debugging;

simplified is_stale, check_stale; fixed map_sg -- proper treatment of non-drafts;

updated;

axioms: NameSpace.table;

PureThy.all_thms_of;

Theory.all_axioms_of, PureThy.all_thms_of;

can (Thm.get_axiom_i thy) name; removed duplicate code;

renamed extern to extern_thm; renamed cert/read_typ_raw to cert/read_typ_abbrev; added cert/read_typ_syntax; thms: NameSpace.table;

meths: NameSpace.table;

NameSpace.extern_table; ProofContext.extern_thm;

Args.local_typ_abbrev;

attribs: NameSpace.table;

renamed global/local_typ_raw to global/local_typ_abbrev;

added structure Inttab; tuned comments;

added type NameSpace.table with basic operations;

renamed cert_typ_raw to cert_typ_abbrev; renamed add_abbrs to add_abbrevs; tuned;

axioms and oracles: NameSpace.table; added axioms_of, all_axioms_of;

map_typ and map_term no longer global;

Major cleanup: got rid of types bclass, xclass, xsort, xtyp, xterm; reorganized code to separate stamps/data/sign; clarified name space inter/extern operations; sane read/certify operations -- more picky about stale signatures; sane implementation of signature extensions;

thms_of no longer global; added all_thms_of; theorems: NameSpace.table;

NameSpace.extern_table;

print_theory: omit name spaces; NameSpace.extern_table;

got rid of bclass, xclass;

add_axioms_infer -- avoids use of stale theory;

Theory.all_axioms_of;

Sign.read_typ_abbrev;

added chmod for packages

added CONTRIBUTORS

a very little cleanup

make up_eq and up_less into simp rules