generalize lemma Lim_unique to t2_space

less ambitious ML_OPTIONS;

another attempt to get a reduced at-sml-dev-e test;

added names, abbrevs;

added completions; misc simplification via aux. operations;

reorganized and abstracted version, via Set trait;

Efficient scanning of literals.

merged

override toplevel "use" functions last;

made SML/NJ happy;

Quickcheck.random

authentic syntax for Pow and image

permissive code attribute; all_eqns

hide constant Quickcheck.random

more parallel stats;

merged

made SML/NJ happy

skip_proof not operative here

where there is nothing, nothing can be hidden

axclass command now legacy

using skip_proof where appropriate

dropped select_default

removed obsolete depend, add_job_acyclic; enqueue, finished: more careful update of cache;

simplified join: do not record dependencies (which are slow, but were only required for dequeue_towards);

back to default -M max, with more robust interpretation of corresponding max_threads value;

merged

dropped diagnostic handles

merged

merged

using SkipProof where appropriate

quickcheck using generic code generator

quickcheck generators for datatypes with functions

more convenient signature for random_fun_lift

improved correctness of get_first (boundary check);

more isatest platforms;

tuned join: produce less garbage while waiting;

improved get_first: check boundary before entering subtrees;

simplified join_results: no longer work "towards" deps, which simplifies task queue management and maintains strict bottom up discipline (without "transfer of priority" to required futures); more efficient Task_Queue.dequeue, with internal cache (reduces wast of cycles with many idle workers); removed complicated/expensive Task_Queue.dequeue_towards;

native get_first, with optional boundary; tuned signature;

moved at-mac-poly-5.1-para back to macbroy6, for continous performance figures;

merged

merged

merged

explicit instantiation yields considerable speedup

separate directory for datatype package

tuned whitespace

correct check for instantiatability

tuned order

merged

separate directory for datatype package

separate directory for datatype package

revised interpretation combinator for datatype constructions

tuned header

merged

merged

tuned make/map/merge combinators

corrected printing of record labels

tuned author list

tuned whitespace

first running version of qc generators for datatypes

less brackets

merged

generalize lemmas about inner

replace all occurrences of dot at type real^'n with inner

declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]

avoid using vec1 in continuity lemmas

add lemma tendsto_setsum

remove simp add: norm_scaleR

declare norm_scaleR [simp]; declare scaleR_cancel lemmas [simp]

replace all occurrences of 'op *s' at type real^'n with scaleR

proper ISABELLE_HOME_USER;

eliminated obsolete CVS2CL;

eliminated cvs ids;

more isatests; macbroy23: nice at-sml-dev-e;

added cases to code_pred command

merged

merged

added lemma

added lemma

masking proof with a quick-and-dirty step

merged

improved infrastructure of predicate compiler for adding manual introduction rules

merged

move lemma compact_Times; generalize more lemmas

generalize lemma edelstein_fix

generalize lemmas

add lemmas about closed sets

new lemmas

new lemmas

theorem attribute [tendsto_intros]

subsection for real instances; new lemmas for open sets of reals

cleaned up some proofs

new lemmas

rewrite proof of compact_convex_combinations to avoid pastecart and vec1

heine_borel instance for products

use constants subseq, incseq, monoseq

remove uses of vec1 in continuity lemmas

two finiteness lemmas by Robert Himmelmann

merged, reverting workarounds on both sides;

theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;

added sporadic (Local)Theory.checkpoint, to enable parallel proof checking;

merged

merged

making isatest happy; but misunderstanding remains

code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function

tuned; corrected exception handling

tuned;

discontinued escaped symbols; tuned;

eliminated escaped symbols;

discontinued escaped symbols such as \\<forall> -- only one backslash should be used;

updated generated files;

allow Isabelle symbols within low-level ML source;

reraise exceptions to preserve position information;

simplified Graph.extend;

removed unused make; simplified extend: eliminated builtin fold, eliminated performance leak (slow member/keys and redundant explore); observe naming conventions of this module;

merged

merged

instance heine_borel < complete_space; generalize many lemmas to class heine_borel

new class heine_borel for lemma bounded_closed_imp_compact; instances for real, ^

generalize compact/closure lemmas