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;

Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;

actually declare "_constrainAbs" as @{syntax_const};

merged

repaired attribute code_unfold_post which has ever been broken

tuned text segment

merged

factored out generic part of Scala serializer into code_namespace.ML

merged

do not print object frame around Scala includes -- this is in the responsibility of the user

repaired codegen tool

tuned internally and made smlnj happy

merged

renewing specifications in HOL-Auth

adapting and tuning example theories

adding further example for quickcheck with prolog code generation

handling the quickcheck result no counterexample more correctly

adding manual reordering of premises to prolog generation

towards support of limited predicates for mutually recursive predicates

improving clash-free naming of variables and preds in code_prolog

exporting mode analysis for use in prolog generation

renaming

improving naming of predicates in code_prolog; changing order of flattened premises once again

changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system

added further hotel key card attack in example file

avoiding warning for a duplicate rewrite rule in preprocessing of the predicate compiler

using Cache_IO interface for a safe parallel prolog execution

storing options for prolog code generation in the theory

adapting example files to latest changes

adding Lambda example theory; tuned

added quite adhoc logic program transformations limited_predicates and replacements of predicates

distinguish between "by" and "apply"

merged

fiddling with "try"

updated