updated generated files;

proper treatment of empty name -- avoid excessive vertical space;

final \makeatother -- catcodes appear to be global;

fixed long name truncation logic

some documentation of @{rail} antiquotation;

more precise source position for @{rail};

sane paragraph layout;

updated configuration options -- no ML here;

tag ML as in IsarImplementation;

treat underscore as in IsarRef;

reactivated codegen example based on Lambda.thy;

formal Base theory;

reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"

whitespace tuning

make SML/NJ happiest

no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter

replaced some Unsynchronized.refs with Config.Ts

do not declare TPTP built-ins, e.g. $true

SNARK workaround

better default type systems for SNARK and ToFoF

tuning

recognize simplification rules even if they look a bit different from the theorems in the theories (meta equality, variable numbers)

generate tags for simps, intros, and elims in TPTP poblems on demand

proper default for TPTP source filed

have each ATP filter out dangerous facts for themselves, based on their type system

eliminated old CVS Ids;

no use of package rail;

obsolete;

removed rail garbage;

NEWS;

just one railsetup.sty which is shipped with the official distribution to accompany @{rail} in Pure;

proper treatment of underscore in rail diagrams;

simplified rail setup, using plain defaults (NB: \small is incompatible with \isabellestyle used here);

eliminated external rail executable;

removed obsolete rail diagrams (which were about old-style theory syntax);

moved material about old codegen to isar-ref manual; eliminated old rail diagram;

eliminated some duplicate "def" positions;

'axiomatization' is global;

discontinued old version of old HOL manual;

merged

removed obsolete rail setup;

uniform content markup;

eliminated obsolete rail macros;

removed obsolete rail diagram (which was about old-style theory syntax);

eliminated separate rail/latex phase;

more precise rail diagrams; misc tuning;

added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;

make SML/NJ happier

make "debug" more verbose and "verbose" less verbose

use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used

cosmetics

supply type-system defaults for major ATPs

make sure that "file" annotations are read correctly in SInE-E and E proofs

fixed random number invocation

make sure E type information constants are given a weight, even if they don't appear anywhere else

fix ROOT.ML and handle "readable_names" reference slightly more cleanly

show sorts not just types in Isar proofs + tuning

Vampire sometimes generates formulas with ~ (not) followed by a quantified subformula, without parentheses -- parse these correctly

tuning

make SML/NJ happy