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