renaming variables to conform to prolog names

changing hotel trace definition; adding simple handling of numerals on natural numbers

added quickcheck generator for prolog generation; first example of counterexample search with prolog for hotel key card system

moving preprocessing to values in prolog generation

invocation of values for prolog execution does not require invocation of code_pred anymore

adding hotel keycard example for prolog generation

improving output of set comprehensions; adding style_check flags

improving ensure_groundness in prolog generation; added further example

adding very basic transformation to ensure groundness before negations

Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;

tuned signature;

Pretty: tuned markup objects;

tuned;

organized markup properties via apply/unapply patterns;

added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;

ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;

merged

tuned code

quotient package: deal correctly with frees in lifted theorems

approximation_oracle: actually match true/false in ML, not arbitrary values;

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

more precise Command.State accumulation;

eliminated some old camel case stuff;

some attempts to recover Isabelle/ML style from the depths of time;

keep persistent production tables as immutable vectors -- potential performance improvement on modern hardware;

select tangible text ranges here -- more robust against ongoing changes of the markup query model

structure Thm: less pervasive names;

discontinued obsolete 'global' and 'local' commands;

merged

merged

moved generic lemmas in Probability to HOL

merged

traling newline on standard output

Quotient Package / lemma for regularization of bex1_rel for equivalence relations

merged

make Mirabelle happy

compute names lazily; there's no point to compute the names of 10000 facts when only 500 are used

clean handling of whether a fact is chained or not; more elegant and reliable than encoding it in the name

don't backtick facts that contain schematic variables, since this doesn't work (for some reason)

quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")

revert this idea of automatically invoking "metisFT" when "metis" fails; there are very few good reasons why "metisFT" should succeed when "metis" fails, and "metisFT" tends to "diverge" more often than "metis -- furthermore the exception handling code wasn't working properly

use matching of types than just equality - this is needed in nominal to cope with type variables

merge

cosmetics

use a soft time limit for E with a hard limit, "eproof"/"eproof.pl" doesn't show the proof is there's less than 1 second left, yielding "the ATP output is malformed"

make remote ATP versions more robust, by starting with "preferred" version numbers and falling back on any version

cosmetics

optimize fact filter some more

cache previous iteration's weights, and keep track of what's dirty and what's clean; this speeds up the relevance filter significantly

modified relevance filter

adjust fudge factors in the light of experiments

invert semantics of "relevance_convergence", to make it more intuitive

if no facts were selected on first iteration, try again with a lower threshold

weed out junk in relevance filter

no need for "eq" facts -- good old "=" is good enough for us

revert unintended change

destroy elim rules before checking for finite exhaustive facts

prevent double inclusion of the fact "True_or_False" in TPTP problems

merged

tuned

merged

dropped pre_post_conv

use conv alias

preliminary versions of static_eval_conv(_simple)

use Code_Thingol.static_eval_conv_simple

added static_eval_conv

refined and unified naming convention for dynamic code evaluation techniques

tap_thy conversional

dropped now obsolete purge_data -- happens implicitly on change of theory identity

merged

introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets

added support for xsymbol syntax for mode annotations in code_pred command

tuned raw Sidekick output;

Text.Range.is_singleton;

Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;

tuned;

Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree; tuned;

tuned root markup;

misc tuning of important special cases;

Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.

merged

merged

use different name for debugging purposes

perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later; it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes

"no_atp" fact that leads to unsound Sledgehammer proofs

"no_atp" fact that leads to unsound proofs in Sledgehammer

"no_atp" fact that leads to unsound proofs

"no_atp" a few facts that often lead to unsound proofs

play with fudge factor + parse one more Vampire error

fiddle a bit with the SPASS fudge number

be more generous towards SPASS's -SOS mode

don't penalize abstractions in relevance filter + support nameless `foo`-style facts

merged

dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates

Document_Model.token_marker: lock jEdit buffer here, which is presumably a critical spot (the model is not necessarily accessed from the Swing thread);

sporadic locking of jEdit buffer;

main session actor as independent thread, to avoid starvation via regular worker pool; tuned;

optional daemon flag;

tuned;

module for simplified thread operations (Scala version);

added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);

recognize more "smlnj" variants;

merged

treat "using X by metis" (more or less) the same as "by (metis X)"

prefer TPTP "conjecture" tag to "hypothesis" on ATPs where this is possible; the disjunctive view of "conjecture" is nonstandard but taken by E, SPASS, Vampire, etc.

merged

more work on finite axiom detection

revert junk submitted by mistake

make sure minimizer facts go through "transform_elim_theorems"

use a smaller simpset in order to not solve refl-instances

allow for pre-simplification of lifted theorems

changed to a more convenient argument order

merged

split and enriched theory SetsAndFunctions

more concise characterization of of_nat operation and class semiring_char_0

inj_comp and inj_fun

tuned: less formal noise in Named_Target, more coherence in Class

remove trivial facts

unbreak "only" option of Sledgehammer

merged