tuned pointer_eq;

renamed data kind;

removed proof data (see Pure/context.ML);

added depth_of;

removed obsolete object.ML (see Pure/library.ML);

export sort_ord; tuned term_ord, typ_ord: use pointer_eq; tuned aconv, aconvs: based on term_ord;

renamed init to init_data;

added structure Object (from Pure/General/object.ML);

tuned;

begin_thy: merge maximal imports; incorporate proof data; added generic context;

removed Pure/Isar/proof_data.ML, Pure/General/object.ML;

improved proof;

obsolete (see Pure/context.ML);

tuned;

pointer equality for sml/nj

(initial commit)

(initial commit)

(initial commit)

(initial commit)

*** empty log message ***

tuned

added -H false

Integrated vampire lemma code.

*** empty log message ***

added find thms section

proper implementation of pointer_eq;

tuned pointer_eq;

VAMPIRE_HOME, helper_path and various stylistic tweaks

lemma, equation between rtrancl and trancl

enter_thms: use theorem database of thy *after* attribute application;

tuned;

added subset, eq_set; tuned insert/remove: avoid garbage;

tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;

fixed HOL-Complex-Matrix target;

removed mkcontent from makedist

fix 'give up waiting message' (logs of running processes are not attached)

* Pure: get_thm interface expects datatype thmref; * More efficient treatment of intermediate theory checkpoints;

avoid identifier 'Name';

Theory.begin/end_theory;

clarify empty vs. pure browser info;

added pointer_eq;

thmref: Name vs. NameSelection; tuned;

refl_tac: avoid failure of unification, i.e. confusing trace msg; get_thm(s): Name;

print_theorems: proper use of PureThy.print_theorems_diff;

thmref: Name vs. NameSelection;

generalized type of inter; added substract; economize heap usage;

added previous;

added begin_theory, end_theory;

added certify_prop, cert_term, cert_prop;

datatype thmref = Name ... | NameSelection ...; added print_theorems_diff; tuned;

added member, option_ord;

OrdList.inter;

tuned;

improved treatment of intermediate checkpoints: actual copy instead of extend, purge after end; tuned;

added add_fixrec_i, add_fixpat_i; ThyParse obsolete; Sign.read_prop, Sign.cert_prop;

proper header;

get_thm(s): Name;

get_thm instead of obsolete Goals.get_thm; improved msg;

HOL-Matrix: plain session;

removed obsolete print_depth;

be less ambitious about the author's name; tuned generated root.tex;

exclude pghead.pdf from doc;

improved formatting;

use Tools/ATP/VampCommunication.ML;

Added VampCommunication.ML. Changed small set of Spass rules to Ordered version. Fixed printing out of resolution proofs if parsing/translation fails.

moved configure to lib/scripts;

./configure obsolete on virtually all systems, but apt to cause problems;

using TPTP2X_HOME; indentation, etc

fixed a faulty proof

moving some generic inequalities from integer arith to nat arith

(moved to Distribution/lib/scripts)

added fixheaders

improved comment;

some minor adaptions to make it work again;

tuned;

tuned remove;

added member;

added Pure/General/ord_list.ML;

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;