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

merged

added Landau theory

added/moved lemmas by Andreas Lochbihler

added Fin_Fun theory

tuned code generator test theories

OCaml builtin intergers are elusive; avoid

more aggresive bracketing of let expressions

tuned whitespace

merged

merged

merged

merged

merged

Reverses idempotent; radical of E; generalized logarithm;

made SML/NJ happy;

merged

use algebra_simps instead of ring_simps

merged, resolving conflict in src/Pure/Isar/attrib.ML;

Generalized Integral_add

Added theorems about distinct & concat, map & replicate and concat & replicate

merged

Fixed broken code dealing with alternative names.

Enclosed parts of subsection in @{text ...} to make LaTeX happy.