add binder syntax for flift1

add new file to test fixrec package

add csplit3, ssplit3, fup3 as simp rules

New features: permissive option for fixrec to skip proofs of equations; side conditions for fixrec equations (for definedness); fixpat theorem names apply to entire group of theorems; improved error messages

added match functions for spair, sinl, sinr

fixed \<Prod> syntax

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;

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;