newref -> new_Addr

renamings: real_of_nat, real_of_int -> (overloaded) real inf_close -> approx SReal -> Reals SNat -> Nats

renamed Product_Type.split to split_conv;

use Syntax.read_xnum;

tuned examples;

* HOL/datatype: induction rule for arbitrarily branching datatypes is now expressed as a proper nested rule (old-style tactic scripts may require atomize_strip_tac to cope with non-atomic premises); * HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule to "split_conv" (old name still available for compatibility); * HOL: improved concrete syntax for strings (e.g. allows translation rules with string literals);

use_text etc.: proper output of error messages;

export fold_ast etc.;