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;

allow nested @{antiq} (nonterminal) and @@{antiq} terminal;

tuned;

more robust error handling (NB: Source.source requires total scanner or recover); tuned;

removed old rail.ML;

railroad diagrams in LaTeX as document antiquotation;

more uniform variations of scan_string;

literal facts `prop` may contain dummy patterns;

eliminated slightly odd Proof_Context.bind_fixes; tuned;

merged

Properly treat proof functions with no arguments.

merged

inlined Function_Lib.replace_frees, which is used only once

more precise positions via binding;

clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;

tuned signature -- eliminated odd comment;

more informative markup for fixed variables (via name space entry); uniform markup for undeclared entities; tuned;

discontinued obsolete markup;

more precise position information via Variable.add_fixes_binding;

more formal treatment of parameters, avoiding slightly odd Variable.intern_fixed;

some adhoc renaming, to accomodate more strict checks of fixes (cf. 4638622bcaa1);

reorganized fixes as specialized (global) name space;

export Name_Space.entry_ord;

direct use of Variable.is_fixed;

tuned;

predefined LaTeX macros for \<bind> and \<then>;

eliminated obsolete Function_Lib.frees_in_term; simplified;

more uniform Variable.add_frees/add_fixed etc.;

structure Cla as defined in FOL;

proper antiquotations;

tuned;

modernized Clasimp setup;

simplified Blast setup;

clarified auxiliary structure Lexicon.Syntax;

simplified/modernized method setup;

simplified/modernized method setup;

mark thm tag "kind" as legacy;

mutabelle reports: parse results out of log file

hardwired mapping "_" -> "Pure.asm_rl" avoids legacy binding;

more precise error positions;

clarified Consts.read_const;

clarified Type.the_decl;

more reports and error positions;

added Name_Space.check/get convenience;

clarified check_simproc (with report) vs. the_simproc; proper report for @{simproc} (NB: ML environment is built in invisible context); only one data slot for this module;

proper binding/report of defined simprocs; tuned signature;

modernized specifications;

tuned signature;

stats for mac-poly-M2;

simplified Data signature;

misc tuning and simplification;

misc tuning;

do not open ML structures;

proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;

modernized Quantifier1 simproc setup;

tuned signature;

clarified simpset setup; discontinued unused old-style FOL_css;

iterate the unsound-fact-set removal process to recover even more unsound proofs

automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option

automatically retry with full-types upon unsound proof

detect some unsound proofs before showing them to the user

tuning -- local semicolon consistency

tuning

rewording

fixed interaction between monomorphization and slicing for ATPs

cleanup: get rid of "may_slice" arguments without changing semantics

implemented general slicing for ATPs, especially E 1.2w and above

fixed typo in documentation

more robust scanning of iterated comments, such as "(* (**) (**) *)";

discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;

eliminated Display.string_of_thm_without_context; tuned whitespace;

merged;

merged

worked around Kodkodi limitation with parsing {}, where it cannot easily deduce its arity -- without this workaround, Kodkod sometimes generates arity errors in conjunction with the "need" option since change 614ff13dc5d2

adding two further code-generator internal constants to the blacklist of Mutabelle

adding examples for Quickcheck used within locales

handling the case where quickcheck is used in a locale with no known interpretation user-friendly

added template diff against newer mercurials, where the 'ago' duplication has been fixed

use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations

hg template diff: renamed to reflect the base version (which silently changed in caf19101073d, by accident?)

standardized some ML aliases;

avoid Display.string_of_thm_without_context; tuned readability of sources;

eliminated global references / critical sections via context data; misc tuning and modernization;

explicit context for Codegen.eval_term etc.;

added Theory.nodes_of convenience;

updated reference machines;

migrated macbroy6 to macbroy30, which is the new "mobile" server (2 cores, 4 GB, Mac OS 10.5);

merged

increase "auto"'s timeout in example to help SML/NJ

making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement

merged

avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary

merged

- renamed enum type class to spark_enum, to avoid confusion with enum type class defined in Enum theory - renamed theorem ..._card_UNIV to ..._card

use "Spec_Rules" for finding axioms -- more reliable and cleaner

optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer

remove a few Nitpick calls in examples -- another step toward making them run faster

check arity of bound variables to avoid generating too large Kodkod problems -- an issue that arose in the context of TPTP/CASC

eliminated Codegen.mode in favour of explicit argument;

less bulky "_position", for improved readability of parse trees;

added more elementary Skip_Proof.make_thm_cterm;

explicit markup for loose bounds;

prefer internal types, via Simple_Syntax.read_typ;

eliminated obsolete Proof_Syntax.strip_sorts_consttypes;

split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;

minor tuning and modernization;

slightly more special eq_list/eq_set, with shortcut involving pointer_eq;

simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;

updated some theory primitives, which now depend on auxiliary context;

more precise treatment of existing type inference parameters; tuned;

pretty_abbrev: read abbreviation more directly;

tuned signature;

raised timeouts further, for SML/NJ!

Package prefix is now taken into account when looking up user-defined types and proof functions.

merged

recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);

scheduler for Mutabelle regression

tool for importing nightly isatest logs

adding bounded_forall tester

creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned

pass plain Proof.context for pretty printing;

standardized aliases of operations on tsig;

pass plain Proof.context for pretty printing;

tuned;

simplified Sorts.class_error: plain Proof.context; tuned;

pass plain Proof.context for pretty printing;

simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;