reference to datatype refinment paper

tuned theory imports

avoid constructor name clash

renamed theory files to be closer to (new) command names

only generate feature weights for queries -- they're not used elsewhere

generate max suggestions in MaSh export driver

new version of MaSh tool, with more server bugfixes

take out dangerous feature, now that all updates are permanent

use new MaSh command-line arguments

shutdown MaSh server

new version of MaSh tool, with less broken server

merged

more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;

proper exhaustive match (cf. e9beabf045ab);

proper context;

merged

renamed theory Mrec to Legacy_Mrec, no longer included by default

replaced use of obsolete MREC by partial_function (heap)

more document antiquotations (for proper theorem names);

moved derivation of strong coinduction to sugar

simpler (forward) derivation of strong (up-to equality) coinduction properties

don't derive unused low-level theorem

tuned example

doc tuning

adapted ML code to new version of MaSh tool

new version of MaSh tool -- experimental server

adapted to new MaSh syntax

tuning

merged

Inserted footnote under match_tac