removed assumption from lemma List.take_add

no need for underscore.sty -- latex.ltx provides \textunderscore and \_ already;

removed \underscoreon which is from Larry's iman.sty, not underscore.sty;

further improved type system setup based on Judgment Days

allow each prover to specify its own formula kind for symbols occurring in the conjecture

better type system setup, based on Judgment Day

improving merge of code specifications by removing code equations of constructors after merging two theories

tuned;

tuned some syntax names;

tuned rail diagrams and layout;

merged;

tuning

reintroduce unsoundnesses taken out in 4d29b4785f43 and 3c2baf9b3c61 but only for unsound type systems

added FIXME

no lies in debug output (e.g. "slice 2 of 1")

help SOS by ensuring that typing information is marked as part of the conjecture + be more precise w.r.t. typedefs in monotonicity check

query typedefs as well for monotonicity

adding examples for invoking quickcheck with records

adding creation of exhaustive generators for records; simplifying dependencies in Main theory

hopefully this will help the SML/NJ type inference

reverted 6efda6167e5d because unsound -- Vampire found a counterexample

improve suggested type system list based on evaluation

I have an intuition that it's sound to omit the first type arg of an hAPP -- and this reduces the size of monomorphized problems quite a bit

removed unsound hAPP optimization

versions of ! and ? for the ASCII-challenged Mirabelle

smoother handling of ! and ? in type system names

tuning

compile + added monotonicity tests

documentation tuning

renamed "many_typed" to "simple" (as in simple types)

update type system documentation

added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)

document monotonic type systems

exploit inferred monotonicity

[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;

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

added TPTP exporter facility -- useful to do experiments with machine learning

renamed theory to make its purpose clearer

fixing typo

improving naming of fresh variables in OCaml serializer

adding code generation setup for String.implode and String.explode in OCaml (contributed by Andreas Lochbihler)

merged;

modernized rail diagrams using @{rail} antiquotation;

tuning

fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs