accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; proper treatment of Pure session;

accomodate identification of type Sign.sg and theory;

accomodate change of TheoryDataFun;

renamed sg_ref to thy_ref;

obsolete;

obsolete (see context.ML);

(removed experimental file)

updated;

Multiple subgoals working.

migrated theory headers to new format

grammar fix

removed redundant "open" declarations

tuned;

a few new integer lemmas

*** empty log message ***

isa-migrate ++

*** empty log message ***

*** empty log message ***

isa-migrate ++

isa-migrate ++

isa-migrate ++

added macos emacs hints

isa-migrate ++

Domain package uses ContProc for beta reduction

allow theorem attributes on fixpat declarations

fixrec package now handles mutually-recursive definitions

(undone experimental changes)

subclassing done

int -> IntInf.int

added lemmas

*** empty log message ***

documented DUMMY

in domain declarations, selector names are now optional

use POLY instead of DISCGARB;

discontinued polyml-3.x; made cygwin functionality less intrusive; more quoting of expressions;

export cases_tac, induct_tac;

added type tactic;

int --> IntInt.int

renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda

cleaned up and reorganized

moved continuity simproc to a separate file

up_eq and up_less in default simpset now

internalize axiom names in Defs.define; compress types via Term.compress_type

downgraded to pdf v 1.4

experimental

just non_functional experimantal code, by now

changed -1 back to 0

more timing information

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

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 ***