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;