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

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.

extended readme

started migration framwork script

added basics for generic migration tool

added isatest-lint prototype

1) Fixed bug in Defs.merge_edges_1. 2) Major optimization of Defs.define: do not store dependencies between constants that cannot introduce cycles anyway. In that way, the cycle test adds almost no overhead to theories that define their constants in HOL-light / HOL4 style. 3) Cleaned up Defs.graph, no superfluous name tags are stored anymore.

*** empty log message ***

updating...

Added the t = x "fix" - in (* ... *) :-(

copy_dir: be permissive wrt. errors;

integrated MacOS X installation instructions

(cvs removed)

migrated scripts to new webiste

minor refinements

Some error messages have been eliminated as suggested by Tobias Nipkow

junk

update -> use

refinements