addressed rare case where the same symbol would be treated alternately as a function and as a predicate -- adding "top2I top_boolI" to a problem that didn't talk about "top" was a way to trigger the issue

added Nitpick limitations to docs

more defensive Nitpick setup -- exotic types of recursion are not supported yet in the model finder

keep temporary error handling in there until code equations are properly generated

tuning (simplified parts of 92c5bd3b342d)

tuning

stengthened tactic to cope with abort cases

tuned names

strengthened tactic w.r.t. "let"

more prominent MaSh errors

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);

updated for release;

updated for release;

updated to sumatra_pdf-2.3.2;

low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;

backout c6297fa1031a -- strange parsers are required to make this work;

make SML/NJ more happy;

enforce IsabelleText font for better symbol coverage, especially on Windows;

proper wrapper for parser -- more explicit error;

misc tuning for release;

remove remains from WinRun4J;

proper document markup;

uniform $ISABELLE_HOME on all platforms;

simplified ISABELLE_HOME on Windows (see also 9c8a1b9c0630, 5a7903ba2dac);

update second environment that is used for System.getenv(String);

adhoc update of JVM environment variables, which is relevant for cold start of jEdit;

tuned names

fold and lemmas about cardinality

more robust parser: 'imports' are mandatory except for bootstrapping Pure;

one more unfolding necessary

faster exit in common case

merged

hide coercion

fixed one line that would never have compiled in a typed language + release the lock in case of exceptions

merged

added Bleast code eqns for RBT

added code eqns for bounded LEAST operator

new theory of finite sets as a subtype

new parametricity rules and useful lemmas

allow to specify multiple parametricity transfer rules in lift_definition

merged

generalise lemma

proper latex;

merged

add relator for 'a filter and parametricity theorems

tuned proofs

add lemmas

prefer Code.abort over code_abort

merged

Added Item_Net.retrieve_matching

Added symmetric code_unfold-lemmas for null and is_none

tuned proofs

moved lemma

merged

proper regexp;

added Isabelle/ML example;

updated jedit.jar, jEdit-patched.tar.gz according to 239f8f451976;

workaround for action-bar shortcut on Mac OS X L&F: avoid EnhancedMenuItem.setAccelerator which causes conflict with regular key handling and thus double invocation -- see also jEdit.actionContext (if actionBarVisible view.removeToolBar);

more uniform modes (NB: comments etc. are handled by isabelle.Token_Markup.Marker);

support more brackets (see also 427724cff970, 7bf637b65ba2);

tuned proofs

further strengthening of tactics

merged

add lemmas

strengthened tactic

tuning

avoid calls to nth with ~1

tuning

strengthened tactic

tactic cleanup

made tactic more robust in case somebody specified a discriminator for a one-constructor type

tuning

use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity

generate "sel_splits(_asm)" theorems

generate "sel_exhaust" theorem

merged

obsolete (see also 48d13465c7c7);

prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);

initialize class immediately (potentially more robust);

tuned

strengthen tactic

use needed case theorems

tuning

added data query function

added data query function

tuning

got rid of dependency on silly 'eq_ifI' theorem

more powerful/robust tactics

use standard "split" properties instead of ad hoc "eq_...I"

tuning

made tactic more flexible w.r.t. case expressions and such

simplified code

simplified directory structure;

obsolete (see da57c4912987);

don't generate wrong type

proper handling of abstractions

fixed off-by-one bug

further improved 'code' helper functions

removed spurious recursion

robustness

thread through bound types

killed redundant argument

improved massaging of case expressions

filled in gap in library offering

updated documentation concerning MacOSX plugin 1.3;

merged

bypass Isabelle OSX_Adapter for now -- MacOSX plugin 1.3 manages that better;

include MacOSX plugin by default -- disabled by default to avoid multiplatform confusion;

removed obsolete cobra.jar, js.jar (see also 30de372ca56f); added MacOSX.jar based on SVN 23208 (essentially plugin version 1.3);

merged

tuned

break more conjunctions

move useful functions to library

merge

simplified code

add non-corecursive constructor view theorems to simps

merged

tuned proofs;

explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);

more powerful fold

properly fold over branches