test sml-dev on mac as well

use only 1 CPU on MacOS 10.4.1

use kleing@cse instead of kleing@in.tum.de

use global settings for isatest-doc

export no_type_brackets; accomodate advanced trfuns; tuned;

proper treatment of advanced trfuns: pass thy argument; tuned warning;

transform_failure in translation functions: TRANSLATION_FAIL; proper treatment of advanced trfuns: pass thy argument; tuned bigimpl_ast_tr, impl_ast_tr';

proper treatment of advanced trfuns: pass thy argument; transform_failure in translation functions: TRANSLATION_FAIL; removed obsolete '*** INSUFFICIENT SYNTAX FOR PREFIX APPLICATION ***';

accomodate advanced trfuns;

removed obsolete (un)fold_ast2;

Drule.implies_intr_hyps;

added print': print depending on print_mode;

no Syntax.internal on thesis;

added print_mode three_buffersN and corresponding cond_print;

cond_print for end-of-proof and calculational commands;

added eq; improved copy/copy_dir: only copy if non-eq;

pass thy as explicit argument (the old ref was not safe in conjunction with lazy evaluation -- the unify code could be fooled about the present theory context);

more efficient treatment of shyps and hyps (use ordered lists); added 'sorts' field to cterm; removed obsolete fix_shyps; moved implies_intr_hyps to drule.ML;

Syntax.read thy;

tuned sort_ord: pointer_eq; tuned size_of_term: less stack usage;

removed obsolete eq_sort, mem_sort, subset_sort, eq_set_sort, ins_sort, union_sort, rems_sort; added efficient operations on ordered lists: eq_set, union, subtract, insert_sort/typ(s)/term(s);

eliminated separate syn type -- advanced trfuns already part of Syntax.syntax;

replaced Syntax.simple_pprint_typ by (Sign.pprint_typ ProtoPure.thy);

added implies_intr_hyps (from thm.ML);

added joinable;

stylistic improvements

added project information in overview

added project information in overview

more sophisticated pypager

first-order check now allows quantifiers

stricter first-order check for meson

Constant "If" is now local

more sophisticated pypager

replacing zabs_def by abs_if

introduced a notion of mirrors

some minor improvements

some minor improvements

some minor improvements

some minor improvements

some minor improvements

some minor improvements

some minor improvements

some minor improvements

some minor improvements

some minor improvements

corrected comment

some corrections

export get_calculation;

Added term_lpo

cancels completely within terms as well now.

Changes due to new abel_cancel.ML

use both processors on macbroy5

switch mac test to macbroy5

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;