Added setup for code generator.

Added function unique_strings.

- exported SAME exception - exported functions for normalizing types

Some basic rules are now stored with "open" derivations, to facilitate simplification of proof terms.

Added new files for proof terms.

generated by Session.name;

export name;

cosmetics

removed imname, uncurried Meth

avoid ML bindings;

Implemented indentation schema for conditional rewrite trace.

Traced depth of conditional rewriting

tuned error message;

prefer immediate monos; tuned;

support for absolute namespace entry paths;

Updated proofs to take advantage of additional theorems proved by "typedef"

removed obsolete "arities";

tuned;

corrected initialization of locals, streamlined Impl

corrected semantics of [iff] concerning rules with premises

replaced 1 by 1'

revisions and indexing

added pair_imageI (also as intro rule)

renamed addaltern to addafter, addSaltern to addSafter

added constify_ast_tr;

field_name_ast_tr superceded by constify_ast_tr in Pure;

_constify;

constify numeral tokens in order to allow translations;

* HOL: syntax translations now work properly with numerals and records expressions;

layout, subscripts

[ "$ML_SYSTEM" = polyml-4.1.1 ] && DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 120";

polyml-4.1.1;