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.

removed division_by_zero class requirements from several lemmas

added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas

choose gnuplot terminal by platform

set terminal png color -- works for older versions of gnuplot;

added ZF-UNITY;

tidied

Added in combinator reduction axioms for B' C' and S'. Also split the original reduction axioms into separate files: I+K, B+C, S, B'+C', S'.

make it work on sunbroy2