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.