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;