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

Fixed "axiom" generation for mixed locales with and without predicates.

added some notes

added file acces rights handling

fix usage of inverts lemma, which has fewer premises now

faster proofs of inverts and injects lemmas, with fewer strictness hypotheses

fixed renamed lemma

major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas

added theorems is_ub_range_shift and is_lub_range_shift

added theorems less_sprod, spair_less, spair_eq, spair_inject

renamed theorems less_ssum4a,b,c,d to more meaningful names

added theorem less_cprod

added theorem injection_less

A flag DEFS_CHAIN_HISTORY can be used to improve the error message in case a cycle has been detected. If it is switched off and a cycle has been detected, the user is notified that there is such a flag.