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

use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...

beware of polymorphic types in typed translation symbol declarations -- match alpha-equivalent types and, more importantly, prevent unsoundnesses by generating type constraints on the arguments of a polymorphic symbols (otherwise "hAPP" can be given any result type)

minor doc fixes

adapt to new type system names

restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"

take "partial_types" option with a grain of salt

fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings

close formula universally, to make SPASS happy

fixed embarrassing bug where conjecture and fact offsets were swapped

pick up GaveUp error on SystemOnTPTP

avoid trailing digits for SNARK (type) names -- grr...

document new type system syntax

use ! for mildly unsound and !! for very unsound encodings

use new type system syntax

implement the new ATP type system in Sledgehammer

define type system in ATP module so that ATPs can suggest a type system

made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support

merge symbol declarations that are type-instances of each other -- useful for type system "Args true" with monomorphization turned off

drop even more bound types in symbol declarations -- useful in particular for type system "Args true"

tuning

got rid of one "sym_table" in "prepare_atp_problem" now that proxies are always handled first, and tuned accordingly

drop "fequal" type args for unmangled type systems

recognize more SystemOnTPTP errors

cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0

make sure that fequal keeps its type arguments for mangled type systems

no needless "fequal" proxies if "explicit_apply" is set + always have readable names

shorten readable names -- they can get really long with monomorphization, which actually slows down the ATPs

avoid Type.TYPE_MATCH exception for "True_or_False" for "If"

proper handling of partially applied proxy symbols

make the problems a bit lighter by getting rid of bound quantifiers for monomorphized constants, since these always have the same return type

improve helper type instantiation code

killed needless datatype "combtyp" in Metis

have properly type-instantiated helper facts (combinators and If)

don't destroy sym table entry for special symbols such as "hAPP" if "explicit_apply" is set

better known failure recognition for ToFoF-E

cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation

fixed min-arity computation when "explicit_apply" is specified

fixed "tags" type encoding after latest round of changes

more higher-order tests for Sledgehammer/ATP

added friendly hint when Isar proof is missing

fix handling of proxies after recent drastic changes to the type encodings

added a hint to Metis errors suggesting metisFT -- it sometimes work

reconstruct TFF type predicates correctly for ToFoF

fixed parsing of not in ATP proofs (e.g. ~x | y is (~x) | y, not ~(x | y))

handle special constants correctly in Isar proof reconstruction code, especially type predicates

make sure the minimizer monomorphizes when it should

fixed arity of special constants if "explicit_apply" is set

make sure typing fact names are unique (needed e.g. by SNARK)

minor cleanup

reimplemented the hAPP introduction code so that it's done earlier, when the types are still available

declare TFF types so that SNARK can be used with types

perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it

move type declarations to the front, for TFF-compliance

use postfix syntax for mangled types, for consistency with unmangled

generate typing for "hBOOL" in "Many_Typed" mode + tuning

generate pure TFF problems -- ToFoF doesn't like mixtures of FOF and TFF, even when the two logics coincide (e.g. for ground formulas)

improve version handling -- prefer versions of ToFoF, SInE, and SNARK that are known to work

unprefix evil "fof_" prefix inserted by ToFoF

added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format

fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged

generate TFF type declarations in typed mode

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;