simp_depth now starts at -1 to make it start at 0 ;-)

added ML-Systems/polyml-posix.ML;

pass ml_platform;

Posix patches (from polyml.ML);

some cygwin support;

* Pure/sign/theory: discontinued named name spaces; * Pure: Theory.axioms_of, PureThy.thms_of etc.;

renamed hide_space to hide_names; refer to name spaces values instead of names;

renamed IsarThy.hide_space to IsarThy.hide_names;

name space of classes and types maintained in tsig;

renamed hide_classes/types/consts to hide_XXX_i; added separate hide_classes/types/consts; refer to name spaces values instead of names;

discontinued named name spaces (classK, typeK, constK); name space of classes and types maintained in tsig; read_tyname/read_const now raise ERROR instead of TYPE; tuned;

accomodate changed #classes; tuned;

accomodate changed #classes;

Theory.hide_consts renamed to Theory.hide_consts_i;

refer to name spaces values instead of names;

renamed Sign.intern_tycon to Sign.intern_type;

fixed spelling;

further optimizations of cycle test

tuned

tuning

IntInf change

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

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