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