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

more [code del] declarations

generalize some constants and lemmas to class topological_space

replace class open with class topo

open_dist instance for vectors

instance * :: topological_space

class real_inner derives from open_dist

introduce class topological_space as a superclass of metric_space

Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.

additional debugging

include chain-ths in every prover-call

split preparing clauses and writing problemfile; included results of count_constants in return-type of prover; optionally pass counted constants to prover; removed unused external_prover from signature

merged

merged

instance ^ :: complete_space

instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair

generalize type of constant lim

class complete_space

generalize constant uniformly_continuous_on

generalize more constants

generalize type of bounded

generalize lemma norm_pastecart

generalize lemma norm_triangle_sub

generalize lemma Lim_unique

generalize lemma closed_cball

generalize Lim_transform lemmas

generalize lemma interior_closed_Un_empty_interior

reuse definition of nets from Limits.thy

replace filters with filter bases

generalize type of 'at' to metric_space

redefine nets as filter bases

new lemmas

limits of Pair using filters

Removed usage of reference in reification

corrected spacing in reflection

switch at-sml-dev-e back to full test on macbroy23

IsabelleProcess: emit status "ready" after initialization and reports;

moved restrict_map_insert to theory Map