cleaned up

cleaned up proof of contlub_abstraction

meson method taking an argument list

deleted a redundant "use" line

tidying

stylistic tweaks concerning Find

shortened time out by 3h (gives up at 12:00h now). test should be finished by 10:00h usually.

made su[bp]/isu[bp] behave the same as their bsu[bp]..esu[bp] counterparts, properly respect isastylescript now

needed for Isabelle independent build

added theorems fix_strict, fix_defined, fix_id, fix_const

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;

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

isa-migrate ++

isa-migrate ++

added macos emacs hints

isa-migrate ++

Domain package uses ContProc for beta reduction

allow theorem attributes on fixpat declarations

fixrec package now handles mutually-recursive definitions

(undone experimental changes)

subclassing done

int -> IntInf.int

added lemmas

*** empty log message ***

documented DUMMY

in domain declarations, selector names are now optional

use POLY instead of DISCGARB;

discontinued polyml-3.x; made cygwin functionality less intrusive; more quoting of expressions;

export cases_tac, induct_tac;

added type tactic;

int --> IntInt.int

renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda

cleaned up and reorganized

moved continuity simproc to a separate file

up_eq and up_less in default simpset now

internalize axiom names in Defs.define; compress types via Term.compress_type

downgraded to pdf v 1.4

experimental

just non_functional experimantal code, by now

changed -1 back to 0

more timing information

simp_depth now starts at -1 to make it start at 0 ;-)

added ML-Systems/polyml-posix.ML;

pass ml_platform;

Posix patches (from polyml.ML);

some cygwin support;

* Pure/sign/theory: discontinued named name spaces; * Pure: Theory.axioms_of, PureThy.thms_of etc.;

renamed hide_space to hide_names; refer to name spaces values instead of names;

renamed IsarThy.hide_space to IsarThy.hide_names;

name space of classes and types maintained in tsig;

renamed hide_classes/types/consts to hide_XXX_i; added separate hide_classes/types/consts; refer to name spaces values instead of names;

discontinued named name spaces (classK, typeK, constK); name space of classes and types maintained in tsig; read_tyname/read_const now raise ERROR instead of TYPE; tuned;

accomodate changed #classes; tuned;

accomodate changed #classes;

Theory.hide_consts renamed to Theory.hide_consts_i;

refer to name spaces values instead of names;

renamed Sign.intern_tycon to Sign.intern_type;

fixed spelling;

further optimizations of cycle test

tuned

tuning

IntInf change

All subgoals sent to the watcher at once now. Rules added to parser for Spass proofs. If parsing or translation fails on a proof, the Spass proof is printed out in PG.

added Isar_examples/Drinker.thy;

full Display.pprint_theory for ML toplevel facilitates debugging;

simplified is_stale, check_stale; fixed map_sg -- proper treatment of non-drafts;

updated;

axioms: NameSpace.table;

PureThy.all_thms_of;

Theory.all_axioms_of, PureThy.all_thms_of;

can (Thm.get_axiom_i thy) name; removed duplicate code;

renamed extern to extern_thm; renamed cert/read_typ_raw to cert/read_typ_abbrev; added cert/read_typ_syntax; thms: NameSpace.table;

meths: NameSpace.table;

NameSpace.extern_table; ProofContext.extern_thm;

Args.local_typ_abbrev;

attribs: NameSpace.table;

renamed global/local_typ_raw to global/local_typ_abbrev;

added structure Inttab; tuned comments;