more coherent naming with ML serializer

dropped code_datatype antiquotation

dropped unnecessary ML code

avoid popular infixes

code_reflect: specify module name directly after keyword

NEWS: code_reflect

merged

updated generated file

modernized structure name

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

parentheses around nested cases

merged

add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)

reintroduced short names for HOL->FOL constants; other parts of the code rely on these

save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code

unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)

redo Sledgehammer proofs (and get rid of "neg_clausify")

removed "sorts" option, continued

remove Sledgehammer's "sorts" option to annotate variables with sorts in proof; what we need is smarter type annotations for variables _and_ constants

insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs

support Vampire definitions of constants as "let" constructs in Isar proofs

tuning

redid the proofs with the latest Sledgehammer; both an exercise and (for a few proofs) a demonstration of the new Isar proof code

remove Nitpick functions that are now implemented in Sledgehammer

added total goal count as argument + message when killing ATPs

make Sledgehammer more friendly if no subgoal is left

polish Isar proofs: don't mention facts twice, and don't show one-liner "structured" proofs

reintroduce missing "gen_all_vars" call

fix types of "fix" variables to help proof reconstruction and aid readability

allow schematic variables in types in terms that are reconstructed by Sledgehammer

in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore