Ordered lists without duplicates.

fixrec shows unsolved subgoals when proofs of rewrites fail

make match_rews into simp rules by default

support theorem names and attributes for fixrec equations; also make them into simp rules by default, like primrec does

added match functions for ONE, TT, and FF; added theorem mplus_fail2

updated;

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

Context.names_of;

* Pure/TheoryDataFun: change of the argument structure; * Pure/TheoryDataFun: change of the argument structure -- got rid of Sign.sg;

Sign.root_path, Sign.local_path;

removed obsolete theory_of_sign, theory_of_thm; Context.draftN; Context.begin_theory;

PolyML.Compiler.printInAlphabeticalOrder := false;

Context.DATA_FAIL; accomodate identification of type Sign.sg and theory;

Context.PureN;

RuleCases.tactic; accomodate identification of type Sign.sg and theory;

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

(RAW_)METHOD_CASES: RuleCases.tactic; accomodate change of TheoryDataFun;

Theory.add_typedecls; Sign.local_path;

added map', fold; changed join to pass key;

Table.fold;

Symtab.fold;

type theory, theory_ref, exception THEORY and related operations imported from Context; actual theory content declared as theory data; removed syn_of; import theory operations in SIGN_THEORY from Sign; tuned;

obsolete type sg is now an alias for Context.theory; code and interfaces related to stamps and data now in context.ML; actual signature content declared as theory data; removed type sg_ref (superceded by theory_ref); signature SIGN_THEORY lists theory operations that are duplicated in Theory;

added theorem_space; removed unused extern_thm_sg; accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory; removed theory management (cf. 'history' in context.ML); moved add_typedecls to sign.ML; Sign.init, Theory.init; tuned;

Context.theory_name; tuned;

added serial numbers;

removed obsolete pretty printers for Theory.theory, Sign.sg; added pretty printer for Context.theory (long form of output);

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