New-style versions of these old examples

Rewrite procedure now works for both compact and full proof objects.

escape_mfix;

added literal;

prep_mixfix': proper use of Syntax.literal;

tuned;

mu-syntax for the LEAST operator

Multiset: added the translation Mult(A) => A-||>nat-{0} (which internalises the `multiset' relation). FoldSet: weakened the typing conditions of the function f and (by the way) removed the `locale' declarations.

tuned;

GPLed;