compile -- fix typo introduced in 07a8145aaeba

pass the right theorems to tactic

prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.; generate code-style theorems (currently commented out since this still fails for many cases); filter tautologies (False ==> ...) out of generated theorems;

repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions

simplify fudge factor code

cleanup SMT-related config options

no isar proofs if preplay was not attempted

normalize more equalities

parallelize MeSh

run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway

use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)

minor performance tuning

use plain types instead of dedicated type pattern

duplicate term and type patterns

optimized built-in const check

added TODO

crank up limit a bit -- truly huge background theories are still nearly 3 times larger

higher minimum relevance threshold, to prevent Sledgehammer from taking too long on "lemma False"

minor fact filter speedups

more gracefully handle huge theories in relevance filters

handle huge MaSh requests gracefully

further optimization in relevance filter

further speed up duplicate elimination

more efficient theorem variable normalization

strengthened constructor-view tactic to deal with 'let's

allow 'let's around constructors in constructor view

reword abstract

more primcorec docs

minor doc fix

new topological lemmas; tuned proofs

strengthen the tactics to bring them in sync with the simplifications taking place in the code (and weaken the simplifications a bit -- let's not deal with implies)

generate optimized DNF formula

rationalized negation code

honor externally set MASH_PORT

process code-style inputs

more tracing

more thorough spying

more Sledgehammer spying -- record fact indices

prevent explosion in monomorphizer (e.g. when the facts typerep_int_def typerep_num_def typerep_option_def typerep_node_def are selected)

removed pointless special case

run fewer provers in "try" mode

count remote threads as well when balancing CPU usage -- otherwise jEdit users and other users of the "blocking" mode may have to wait for 2 * timeout if they e.g. have 4 cores and 5 provers (the typical situation)

more parallelism in blocking mode

more robustness in MaSh

back to post-release mode -- after fork point;

tuned;

tuned;

more notes;

tuned;

added and generalised lemmas

Streamlined locales reference material.

merged

tuned

merged

keep the qualification of bindings when noting bnf theorems

strengthened tactic (primcorec_sel_tac) + tuning

renamings

got rid of needless argument

make SMT integration slacker w.r.t. bad apples (facts)

strengthen top sort check

tuned whitespace;

tuned;

unset XMODIFIERS by default, in order to prevent total loss of key events seen on Fedora 18/19;

updated to scala-2.10.3;

tuned;

some highlights of Isabelle2013-1 based on NEWS;

tuned;

misc tuning for release;

more (co)data docs

don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded

NEWS and CONTRIBUTORS

made SML/NJ happy

use new coinduction method and primcorec in examples

new coinduction method

tuned command descriptions

strengthen tactic w.r.t. let

minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)

typo

NEWS and CONTRIBUTORS

merged

compile -- broken since 21dac9a60f0c

strengthened tactic for right-hand sides involving lambdas

basic documentation for function elimination rules and fun_cases

allow uncurried lambda-abstractions on rhs of "primcorec"

tiny doc fix

base the fset bnf on the new FSet theory

improved backwards compatiblity of primrec_new (Isabelle/ML interface, attributes, etc.)

removed spurious save if nothing needs to bee learned

new version of MaSh that really honors the --port option and that checks for file name mismatches

minor textual changes

got rid of dead feature

refactoring -- splitting between constructor sugar dependencies and true BNF dependencies

renamed ML files

renamed theory file

tuned signature -- facilitate experimentation with other processes;

preserve types during rewriting

made SML/NJ happy

made SML/NJ happy

made SML/NJ happier

added experimental configuration options to tune use of builtin symbols in SMT

added possibility to reset builtins (for experimentation)

just one data slot (record) per program unit

more "primrec_new" documentation

merged

tuned signature;

eliminated clone of Inductive.mk_cases_tac;

tuned signature;

tuned whitespace;

provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);

merge

minor tweak to error message

tuned;

explicit caret position after replacement;

tuned proofs

observe user preferences;

updated for release;

tuned;

tuned;

more on text completion;

made SML/NJ happy (NB: toplevel ML environment is unmanaged);