Add lessThan_Suc_eq_insert_0

merged

updated

set printmode while marking

updated

avoid reference to theory Ferrack altogether

more canonical theory setup

set depth to 1

avoid theory Imperative_HOL altogether

adapted to change eq -> equal

corrected printmode handling

swapped slip

updated

restored and added surpression of case combinators

dropped superfluous presentation names

manage statement selection for presentation wholly through markup

formal markup of generated code for statements

removed namespace stuff from code_printer

merged

reenable Nitpick on Cygwin; we'll see tomorrow if there's still a failure, and if so I'll investigate

merged;

Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";

turned show_consts into proper configuration option;

prefer regular Proof.context over background theory; misc tuning and simplification;

just one refute.ML;

use existing Integer.pow, despite its slightly odd argument order;

tuned whitespace and indentation, emphasizing the logical structure of this long text;

inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;

Document_View: squiggly underline for messages; tuned;

added gfx_range convenience;

Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;

Position.Range: exclude singularity (again);

merged

merged

FIXME -> TODO (nothing is broken)

Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF

use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine

make definitional CNF translation code more robust in the presence of existential quantifiers in the "literals"

formal framework for presentation of selected statements

merged

Table.map replaces Table.map'

dropped dead code; tuned

include names need not be considered as reserved any longer

skip empty name bunches; fill up trailing positions with NONEs

use code_namespace module for SML and OCaml code

Table.map replaces Table.map'

avoid cyclic modules

merged

simultaneous modification of statements: statement names

simultaneous modification of statements

explicit modify_stmt parameter

Graph.map, in analogy to Table.map

replaced Table.map' by Table.map

merged

tuned

generalized hierarchical data structure over statements

merged

normalization is allowed to solve True

merged

merged

cosmetics

SNARK doesn't like facts

show real CPU time

factor out code shared by all ATPs so that it's run only once

handle all whitespace, not just ASCII 32

speed up SPASS hack + output time information in "blocking" mode

remove time information in output, since it's confusing anyway

minor refactoring

translate the axioms to FOF once and for all ATPs

run relevance filter in a thread, to avoid blocking

add dependency of "spass" script

more elegant ML

only kill ATP threads in nonblocking mode

lower number of facts given to SInE

share the relevance filter among the provers

got rid of the "theory_relevant" option; instead, have fudge factors that behave more smoothly for all provers

generalize theorem argument parsing syntax

support new option in Mirabelle

fiddled with fudge factor (based on Mirabelle)

give priority to assumptions in structured proofs

introduce fudge factors to deal with "theory const"

rename sledgehammer config attributes

finish moving file

move file

finished renaming

fix typo

shorten a few file names

added "expect" feature of Nitpick to Sledgehammer, for regression testing

update docs

update docs

added "blocking" option to Sledgehammer to run in synchronous mode; sometimes useful, e.g. for testing

normalization fails on unchanged goal

turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;

prefer regular print functions over slightly low-level Term.string_of_vname;

eliminated obsolete old-style goal stack package, which was considered the main Isabelle user interface at some point;

eliminated really ancient OldGoals operations in favour of Goal.prove_internal (with its minimal checks and without normalization of result); tuned white space; tuned indentation;