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"

method linarith

reraise exceptions to preserve position information;

ML_Compiler.exn_message;

ML_Compiler.exn_message;

added exn_message (formerly in toplevel.ML); eval/code: proper Isar runtime support; tuned signature;

moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);

report_parse_tree: ML_open, ML_struct; eval: terminate input by explicit end token, to ensure that Poly/ML attaches proper position to last input token; tuned;

export end_pos_of;

use: tuned error;

added markup ML_open, ML_struct;

use_text: pass file name to compiler, tuned;

tuned comments;

removed obsolete YXML/XML.detect;

Approximation: Corrected precision of ln on all real values

Approximation: Implemented argument reduction for cosine. Sinus is now implemented in terms of cosine. Sqrt computes on the entire real numbers

CONTRIBUTORS

merged

tuned proofs

added mk_valtermify_app and mk_random

Set.insert with authentic syntax

merged

Set.insert with authentic syntax

added trees implementing mappings

avoid Library.foldl_map

class replaces axclass

insert now qualified and with authentic syntax

lemma about List.foldl and Finite_Set.fold

dropped legacy ML bindings; tuned

lemmas about basic set operations and Finite_Set.fold

merged

new lemma

merged

fix type of hnorm

define netlimit in terms of eventually

generalize type of 'at' to topological_space; generalize some lemmas

add extra type constraints for dist, norm

generalize norm method to work over class real_normed_vector

example settings for Poly/ML 5.3 (experimental);

uniform (short) ids on both sides;

merged

finite lemmas

made SML/NJ happy

merged

A few finite lemmas

removed unused location_of; eval: actually pass location properties (via "file" field);

retrieve ML source files;

export file_name;

more robust treatment of bootstrap source positions;

less experimental polyml-5.3;

just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;

exn_message/raised: ML_Compiler.exception_position;

eliminated costly registration of tokens;

convert explicitly between Position.T/PolyML.location, without costly registration of tokens; added exception_position;

added exception_position (dummy);

reraise exceptions to preserve original position (ML system specific);

tuned signature;

export esc;

export value;

uniform default settings for E, Vampire, SPASS;

merged

add classes for t0, t1, and t2 spaces

generalize type of islimpt