explicit @{type_syntax} markup; misc tuning and simplification;

more orthogonal antiquotations for type constructors;

clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;

provide direct access to the different kinds of type declarations;

use mixfix syntax for Boogie types

merged

added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals