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