tuned

NewNumberTheory

Added NewNumberTheory by Jeremy Avigad

fixed thm name

fix name clash with old/new prime libraries

merged

update to work with new GCD library

generalized less_Suc_induct

merged

update ex/Sqrt.thy to use new GCD library

update to use new GCD library

merged

more [code del] declarations

add NatTransfer.thy, needed for new GCD library

merged

new GCD library, courtesy of Jeremy Avigad

replaced java Properties by pure property lists; added offsets_of;

environment: keep original HOME and PATH (required for Cygwin integrity);

added toString;

jar: jvmpath wrapper (requires bash);

subSequence: bounds checking;

added reverse CharSequence;

merged

uncheck is liberal wrt. semityped terms

stripped dead comment

skip_proof where appropriate

more robust poly startup, by restricting heap size (otherwise it fails on very large memory); removed Poly/ML 4.x variant;

merged

end_timing: actually display GC percentage, not factor;

merged

Polishing the English

rtrancl lemmas

made SML/NJ happy;

usedir: internal timing option;

more detailed start_timing/end_timing;

more detailed start_timing/end_timing (in timing.ML); removed obsolete check_timer;

removed obsolete time accumulator (better use Toplevel.profiling);

minor tuning according to Isabelle/ML conventions; slightly less combinators;

back to polyml-5.2.1;

corrected some issues

refined section concerning classes

reworked section on type classes

merged

reworked section on type classes

updated table of overloaded constants

more precise dependencies

fixed grammar

obey SML syntax even more closely

merged

obey SML syntax more closely

datatype packages: record datatype_config for configuration flags; less verbose signatures

merged

ignore in-situ contrib symlinks

datatype packages: record datatype_config for configuration flags; less verbose signatures

dropped ID

denominator should not be zero

tuned brackets for let expressions etc.

merged

smult_dvd lemmas; polynomial gcd

generalize lemmas dvd_mod and dvd_mod_iff to class semiring_div

move lemma div_power into semiring_div context; class ring_div inherits from idom

generalize many constants and lemmas from Convex_Euclidean_Space

generalize lemma connected_real_lemma

generalize lemmas

replace uses of (bi)linear with bounded_(bi)linear

new continuous/vimage lemmas; cleaned up proofs

generalize constants netlimit and continuous

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

add lemma complete_imp_closed

generalize constant 'bounded' to class metric_space

generalize lemmas compact_imp_bounded, compact_imp_closed

generalize more lemmas

generalize constant 'indirection'

lemmas about linear, bilinear

generalize constant 'complete'

generalize lemmas eventually_within_interior, lim_within_interior

generalize more lemmas

generalize some lemmas

avoiding duplicate definitions of executable functions

tuned;

more native Scala style; added is_open; misc tuning;

tuned;

simplified IsabelleSystem.platform_path for cygwin; eliminated ISABELLE_ROOT_JVM; tuned;

merged

removed duplicate lemmas

removed general graph functions in the predicate compiler

added graph builders

removed debug messages

refactoring the predicate compiler

merged

Tuned sos tactic to reject non SOS goals

tuned

fast_lin_arith uses proper multiplication instead of unfolding to additions

more lemmas

Better approximation of cos around pi.

merged

merged

new lemma

merged

merged

proper deresolving of class relations and class parameters in SML

New lemma

eliminated hardwired Cygwin setup;

Accessing the Cygwin installation.

static IsabelleSystem.charset; static IsabelleSystem.is_cygwin -- based on system property "os.name"; smart bootstrapping of Isabelle settings environment (via implicit or explicit ISABELLE_TOOL, or isabelle.tool property, or isabelle via PATH); source_file: removed obsolete special treatment of "ML"; misc tuning and reorganization;

isabelle getenv: option -d;

no parallel make jobs on macbroy23, which is the machine where SML/XL is tested -- attempt to consume less resources;

updated version;

fix type of open

new setL2 lemmas; instance ^ :: (topological_space, finite) topological_space

replace 'topo' with 'open'; add extra type constraint for 'open'

generalize tendsto lemmas for products

move definitions of open, closed to RealVector.thy

lemmas islimptI, islimptE; generalize open_inter_closure_subset

generalize tendsto to class topological_space

put syntax for tendsto in Limits.thy; rename variables

constant "chars" of all characters

added infrastructure for definitorial construction of generators for datatypes

constant "chars" of all characters

added generator for char and trivial generator for String.literal

using constant "chars"