new

Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers. Will now signal if ATP has run out of time and then kill the watcher.

* Pure: the Isar proof context type is already defined early in Pure as Context.proof;

added find2

*** empty log message ***

tunes Find

added Rules/find2

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;