removed pretty_theory, pprint_theory (see context.ML or thy_info.ML); removed obsolete pretty_name_space; accomodate identification of type Sign.sg and theory;

added type theory: generic theory contexts with unique identity, arbitrarily typed data, linear and graph development -- a complete rewrite of code that used to be spread over in sign.ML, theory.ML, theory_data.ML, pure_thy.ML;

removed Pure/theory_data.ML;

added Id;

Theory.merge;

accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Context.theory_name;

Context.theory_name;

accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; Sign.the_const_type; Context.exists_name;

replaced obsolete theory_of_sign by theory_of_thm;

accomodate change of TheoryDataFun; Context.str_of_thy;

refer to HOL4_PROOFS setting; accomodate identification of type Sign.sg and theory;

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