[mq]: nitpick_tuning

fixed cardinality computation for function types such as "'a -> unit"

monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.

proper case_names for int_cases, int_of_nat_induct; tuned some proofs, eliminating (cases, auto) anti-pattern;

added type annotation for SML/NJ

eta-expansion for SML/NJ

removed odd historical material;

merged

fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a

cosmetics

more conventional naming scheme: names_long, names_short, names_unique;

railsetup required for IsarRef/style;

fit page;

use existing \<hyphen>;

more precise syntax diagram;

simplified rail configuration;

provide \isabellestyle{itunderscore} (requires underscore.sty);

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;