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;