add lemmas InfinitesimalI2, InfinitesimalD2

adapted to pre-5.0 versions;

Poly/ML startup script (for 4.9.1);

added ML-Systems/polyml-4.9.1.ML;

Compatibility wrapper for Poly/ML 4.9.1.

removed all references to star_n and FreeUltrafilterNat

add lemmas about hnorm, Infinitesimal

reverted to 1.58;

proper const_syntax for uminus, abs;

reorganized HNatInfinite proofs; simplified and renamed some lemmas

removed obsolete of_instream_slurp -- now already included in tty;

Source.tty now slurps by default;

of_stream/tty: slurp input eagerly;

tuned all_paths;

internal params: Vartab instead of AList;

removed unused serial_of, name_of;

removed redundant lemmas;

remove redundant lemmas

replaced constant 0 by HOL.zero

hypreal_of_nat abbreviates of_nat

add lemmas of_real_eq_star_of, Reals_eq_Standard

move star_of_norm from SEQ.thy to NSA.thy

convert more proofs to transfer principle

add lemmas about Standard, real_of, scaleR

instance complex :: real_normed_field; cleaned up

add lemma stc_unique; shorten stc proofs

add lemmas approx_diff and st_unique, shorten st proofs

add lemmas about of_real and power

reorganize section headings

more lemmas about Standard and star_of

define new constant Standard = range star_of

add lemmas of_int_in_Reals, of_nat_in_Reals

add header

Changed precedence of "op O" (relation composition) from 60 to 75.

handling of \<^const> syntax for case; explicit case names for induction rules for rep_datatype

tuned syntax for <= <

renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes

renamed 0 and 1 to HOL.zero and HOL.one respectivly

fixed the definition of "depth"

Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas

some cleanup

changed order

inserted headings

changed interface in codegen_package.ML

fixed some mess

cleaned up

adding constants the modern way

added examples for variable name handling

better handling for div by zero

updated theory description

refinements in codegen serializer

added 'undefined' serializer

added code_instname

reorganized subsection headings

moved SEQ_Infinitesimal from SEQ to HyperNat

real_norm_def [simp]

generalize types of lim and nslim

generalized types of sums, summable, and suminf

add lemma convergent_Cauchy

remove extra dependencies

add proof of summable_LIMSEQ_zero

change definitions from SOME to THE

move root and sqrt stuff from Transcendental to NthRoot

fix proof

added lemmas about LIMSEQ and norm; simplified some proofs

add lemma norm_power

added HOL-Complex-ex;

define constants with THE instead of SOME

Fixed bug concerning the generation of identifiers for datatypes, which caused the code generator to fail for mutually recursive datatypes.

Replaced irreducible_paths by all_paths.

Added function all_paths (formerly find_paths).

tuned proofs;

tuned oracle name;

added is_ml_reserved;

member (op =); tuned;

serial numbers for types;

added dest_binop;

member (op =); tuned pattern check;

member (op =); Drule.dest_equals_rhs;

tuned eta_contract;

added dest_equals_rhs; moved dest_binop to thm.ML;

tuned;

serial numbers for consts; added serial_of/name_of;

Thm.dest_binop;

member (op =); ThmDatabase.is_ml_reserved; tuned oracle name;

member (op =);

updated timings;

new function hashw_int

Yet another version of fake_thm_name. "Full" hashing ensures that there are no collisions unless theorems differ by sorts alone, which should not matter. Also minor fixes to standard hashing.

corrected for the translation from _ to __ in c_COMBx_e

changed constants into abbreviations; shortened proofs

XML syntax for types, terms, and proofs.

Added xml_syntax.ML

Added Tools/xml_syntax.ML

circumvented defect in SML/NJ type inference

1. Function package accepts a parameter (default "some_term"), which specifies the functions behaviour outside its domain. 2. Bugfix: An exception occured when a function in a mutual definition was declared but no equation was given.