updated SMT module and Sledgehammer to fully open source Z3

updated to new Z3

renamed multiset ordering to free up nice <# etc. symbols for the standard subset

removed TODO

consistent naming

merged

more lemmas and operations on cset (adapted from FSet)

tuned signature;

tuned;

misc tuning for release;

merged

Removed mcard because it is equal to size

generalized slightly

generalized code

generalized code

export ML function

recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;

more qualified names -- eliminated hide_const (open);

tuned;

merged

local setup of induction tools, with restricted access to auxiliary consts; proper antiquotations for formerly inaccessible consts;

support for 'restricted' modifier: only qualified accesses outside the local scope;

tuned;

clarified rail syntax;

@{command_spec} is superseded by @{command_keyword};

clarified command keyword markup;

more position information and PIDE markup for command keywords;

allow prefix before keyword, notably 'private';

support local command setup;

proper header; misc tuning;