reimplemented the hAPP introduction code so that it's done earlier, when the types are still available

declare TFF types so that SNARK can be used with types

perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it

move type declarations to the front, for TFF-compliance

use postfix syntax for mangled types, for consistency with unmangled

generate typing for "hBOOL" in "Many_Typed" mode + tuning

generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)

improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work

unprefix evil "fof_" prefix inserted by ToFoF

added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format

fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged

generate TFF type declarations in typed mode

no point in keeping indices in Sledgehammer readable var names, since these are disambiguated anyway

added more rudimentary type support to Sledgehammer's ATP encoding

fixed type of ATP quantifier types (sic)

added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS

added support for TFF type declarations

reintroduced constructor for formulas, and automatically detect which logic to use (TFF or FOF) to avoid clutter

added room for types in ATP quantifiers

distinguish FOF and TFF (typed first-order) in ATP abstract syntax tree

remove experimental feature ("risky overload")

added (without implementation yet) new type encodings for Sledgehammer/ATP

close ATP formulas universally earlier, so that we can add type predicates

get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables

renamings

tuned;

include static rail files for old manuals, to make standard make job independent of the "rail" executable;

simplified keyword markup (without formal checking);

treat @ as separate keyword; added @'text' for \isakeyword markup;

default rail fonts via isabellestyle;

localized \isabellestyle;

misc cleanup;

misc cleanup -- no need to copy style files;

eliminated copies of isabelle style files;

use @{rail} antiquotation (with some nested markup); eliminated separate rail/latex phase;

updated Variable.focus;

allow nested @{antiq} (nonterminal) and @@{antiq} terminal;

tuned;

more robust error handling (NB: Source.source requires total scanner or recover); tuned;

removed old rail.ML;

railroad diagrams in LaTeX as document antiquotation;

more uniform variations of scan_string;

literal facts `prop` may contain dummy patterns;

eliminated slightly odd Proof_Context.bind_fixes; tuned;

merged

Properly treat proof functions with no arguments.

merged

inlined Function_Lib.replace_frees, which is used only once