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

more precise positions via binding;

clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;

tuned signature -- eliminated odd comment;

more informative markup for fixed variables (via name space entry); uniform markup for undeclared entities; tuned;

discontinued obsolete markup;

more precise position information via Variable.add_fixes_binding;

more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;

some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);

reorganized fixes as specialized (global) name space;

export Name_Space.entry_ord;

direct use of Variable.is_fixed;

tuned;

predefined LaTeX macros for \<bind> and \<then>;

eliminated obsolete Function_Lib.frees_in_term; simplified;

more uniform Variable.add_frees/add_fixed etc.;

structure Cla as defined in FOL;

proper antiquotations;

tuned;

modernized Clasimp setup;

simplified Blast setup;

clarified auxiliary structure Lexicon.Syntax;

simplified/modernized method setup;

simplified/modernized method setup;

mark thm tag "kind" as legacy;