Added new option for setting level of detail for proof objects.

Proof of True_implies_equals is stored with "open" derivation to facilitate simplification of proof terms.

Added code generator setup.

Added new files for code generator.

Renamed functions % and %% to avoid clash with syntax for proof terms.

Adapted to new proof terms.

Exported ml_reserved.

Made consts list operations a bit faster.

Added new argument to use_dir for derivation kind.

Removed tag_assumption.

Tuned naming of theorems.

Added functions for printing primitive proof terms.

Tuned function extend_lexicon.

Initial revision of tools for proof terms.

Now obsolete; replaced by LF style proof terms.

Initial version of generic code generator.

New implementation of LF style proof terms.

Replaced old derivations by proof terms.

Tidied function SELECT_GOAL.

Added equality axioms and initialization of proof term package.

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