use code_reflect

merged

Tuning the quotient examples

clarified signature; simpler implementation in terms of function's tactic interface

return info record (relative to auxiliary context!)

default termination prover as plain tactic

function: sane interface for programmatic use

ML interface uses plain command names, following conventions from typedef

function: better separate Isar integration from actual functionality

merged

export somehow odd mapa explicitly

exported print_tuple

take into account tupled constructors

avoid code_datatype antiquotation

merged

added an example with a free function variable to the Predicate Compile examples

removed local clone in the predicate compiler

improving proof procedure for transforming cases rule in the predicate compiler to handle free variables of function type

allow concrete syntax for local entities within a proof body, either via regular mixfix annotations to 'fix' etc. or the separate 'write' command;

'write': actually observe the proof structure (like 'let' or 'fix');

adapted ProofContext.infer_type;

ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;

avoid clash with keyword 'write';

allow mixfix syntax for fixes within a proof body -- should now work thanks to fully authentic syntax;

uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);

disabled spurious invocation of (interactive) sledgehammer;

merged

make Mirabelle happy

remove removed option

merge