merged

tuned proofs;

print find_thms result in reverse order so best result is on top

more useful sorting of find_thms results

proper sharing after change of directory structure (cf. 32ec957e5c3e); result is structurally equal, despite change of hash key;

restricted heap, which might improve stability of this test;

merged

tuned proofs;

tuned proofs;

updated to jdk-7u40;

added component jdk-7u40.tar.gz (inactive);

merged

more (co)data docs

tuning

more (co)data doc

generalized and simplified proofs of several theorems about convex sets

more (co)data docs

removed accidentally submitted line

more (co)data doc

more general typing of monadic bind

merged

omit automatic Induct.cases_pred declaration, which breaks many existing proofs

NEWS and CONTRIBUTORS

merged

added some examples and tests for fun_cases

dropped unnecessary 'open'

tuned headers

moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information; normalized whitespace and indentation

clarified

clarified, dropping unreachable bool special case

dropped dead code

clarified

generate elim rules for elimination of function equalities; added fun_cases command; recover proper cases rules for mutual recursive case (no sum types)

tuned proofs

merged

make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'

generalize lemmas

remove unneeded assumption from prime_dvd_power lemmas; add iff forms of prime_dvd_power lemmas (thanks to Jason Dagit)

remove duplicate lemmas

new lemmas

prefer theorem name over 'long_thm_list(n)'

prefer attribute 'unfolded thm' to 'simplified'

removed outdated comments

made non-co case more robust as well (cf. b6e2993fd0d3)

don't wrongly destroy sum types in coiterators

beware of multi-constructor datatypes (cf. 27c418b7b985)

beware of single-constructor datatypes, with no discriminators

more robust tactic to cover another corner case (added as example);

generalized data structure, for extension with SMT solver proofs

prefixed types and some functions with "atp_" for disambiguation

merged;

absorb final CLASSPATH as well, such that tools might provide that by elementary means, without the "classpath" shell function (e.g. kodkodi/nitpick);

more CHECKLIST;

more robust System.getProperty with default;

generate distribution classpath for cold-start application wrappers;

reverse orientation of ISABELLE_CLASSPATH;

propagate ISABELLE_CLASSPATH;

tuned comments;

clarified directory structure;

maintain classpath in more elementary manner: turn ISABELLE_CLASSPATH into -classpath option, so that all jars are covered by sun.misc.Launcher.AppClassLoader (e.g. relevant for loading add-on resources); ignore $ISABELLE_JAVA_EXT -- do not change java.ext.dirs;

more official initial class path according to sun.misc.Launcher;

provide main classpath again, notably for cold-start;

cold-start of main application even on Linux;

tuned proofs;

more explicit indication of 'done' as proof script element;

made tactic handle gracefully the case: codatatype ('a, 's) scheduler2 = Combine2 "'s => 'a" "'s => ('a, 's) scheduler2"

conceal definitions of high-level constructors and (co)iterators

conceal low-level noted facts (+ FIXME to get rid of the notes altogether eventually)

buffer the notes even more

conceal internal bindings

add a notice to myself in doc

more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses

unset some spurious executable flags

handle corner case in tactic

simplified derivation of in_rel

removed unused/inlinable theorems

when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated

minor fixes

commented out code parts leading to runtime errors due to missing gensim module

invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)

new version of MaSh

more (co)data docs

avoid a keyword

more (co)datatype docs

killed dead code

get rid of another complication in relevance filter

tuning

renamed config option

more correct NEWS

kick out totally hopeless facts after 5 iterations to speed things up

reintroduced 8d8f72aa5c0b, which does make a small difference in practice, but implemented more efficiently

more (co)data docs

more (co)data docs

more (co)data docs

merged

prefer explicit type constraint (again, see also Type.appl_error); pretty const with markup; clarified "the context";

tuned signature;

tuned whitespace;

tuned message;

do not expose internal flags to attribute name space;

more (co)data docs

more (co)datatype documentation

tuning

disable some checks for huge background theories

tuning

reintroduced half of f99ee3adb81d -- that part definitely looks useless (and is inefficient)

reverted f99ee3adb81d -- that old logic seems to make a difference still today

merged

tuned comment;

tuned;

updated for release;

tuned proofs;

tuned proofs;

updated to jedit_build-20130910 (with update of jedit.jar and Highlight.jar);

disable some key event workarounds going back to Matthieu Casanova (08-Dec-2007) and Slava Pestov (until 2005) -- lets hope that Java 7 works more uniformly with numeric keypads;

tuned proofs;

discontinued obsolete command-line tool "isabelle build_dialog";

updated docs

speed up often-called function

got rid of currently unused data structure, to speed up relevance filter

adjusted number of generated monomorphic instances for new monomorphizer based on new evaluation (E, SPASS, Vampire)

sorted out dependencies

faster detection of tautologies

slight speed optimization

got rid of another slowdown factor in relevance filter

removed completely needless, inefficient code

minor speed optimization

got rid of another taboo that appears to make no difference in practice (and that slows down the relevance filter)

avoid double traversal of term

got rid of old, needless logic

moved ML function closer to its remaining use

faster uniquification

stronger fact normalization

gracefully handle huge thys

speed up detection of simp rules

don't be so verbose about SMT solver failures

tuned;

more portable hash-bang;

tuned signature;

merged

tuned proofs;

tuned proofs;

make facts like "mem_Collect_eq" more likely to be picked up by few-fact slices

since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion

more docs

merged

proper apple.awt.application.name for Java 7;

generate application Info.plist based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);

more robust Mac OS X application support;

use polyml-5.5.1 (SVN), to increase chances of stability of this test;

override potential changes in $ISABELLE_HOME_USER/etc/settings;

generate application ini based on $ISABELLE_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also lib/Tools/java and src/Tools/jEdit/lib/Tools/jedit);

generate application based on $JEDIT_JAVA_OPTIONS $JEDIT_SYSTEM_OPTIONS at build time (see also src/Tools/jEdit/lib/Tools/jedit);

tuning

made semantics of "max_new_instances" be what the name suggests, the previous implementation did, and the Sledgehammer manual documents

limit the number of instances of a single theorem

move metis to new monomorphizer

use new monomorphizer in Sledgehammer

tuning

include map theorems in datastructure for "primcorec"

enriched data structure with necessary theorems

updated exe -- more explicit icon;

more official lib/logo/isabelle.bmp;

use windows_app based on WinRun4J;

updated to WinRun4J;

tuned whitespace

don't register "sequential" as a keyword for now as this breaks the parser for function

tuned proofs;

merged

tuned message;

tuned message;

imitate "isabelle java" and "isabelle jedit" wrt. classpath and options (see also a221a4fdb5a0);

generate application wrapper for Linux;

observe "stopped" after Cygwin init (which is itself uninterruptible);

clarified modules;

tuned signature;

Cygwin_Init based on System_Dialog;

tuned imports;

more robust exit;

Build_Dialog based on System_Dialog; avoid hopping between threads;

clarified close operations;

clarified result;

dialog for system processes, with optional output window;

more portable access to icon -- avoid Isabelle_System which is not yet initialized in bootstrap;

odd workaround for scalac to enable nohup;

odd workaround for scalac to enable nohup;

build session before start of jedit;

imitate "isabelle java" and "isabelle jedit" wrt. classpath and options;

more Proof General legacy;

use JEDIT_OPTIONS only once (in isabelle.Main.start_jedit);

warm start of Isabelle/jEdit from Isabelle/Scala; avoid mass confusion of plugins due to change of -classpath (cf. 5bef05f5ed58);

prefer explicit thread;

tuned proofs;

tuned proofs;

prefer Isabelle/Scala over bash; actual platform_path (in contrast to eb8806a2e348);

prefer Isabelle/Scala over bash;

prefer warm start via JEdit_Main;

slight cleanup of lemma locations; tuned proof

tuned

tuned;

tuned;

removed junk;

more standard header;

updated keywords;

merged

added examples for Simps_Case_Conv

allowed less exhaustive patterns

use case_of_simps

use case_of_simps

added simps_of_case and case_of_simps to convert between simps and case rules

merged

close window and start process asynchronously;

more explicit cygwin_root (again) -- do not rely on isabelle_home as cwd;

recovered cygwin.root from 1c87e79bb838; removed junk;

provide file indicator;

updated windows_app-20130905;

main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator; standardized jdk location;

standardize jdk name; check tar errors;

updated to jdk-7u25; less redundant directory structure;

support only one scala version; tuned;

updated to jedit_build-20130905 which is based on jedit-5.1.0; added jsr305-2.0.0.jar from http://code.google.com/p/findbugs (via ivy cache), which is required to resolve javax.annotation.*;

explicit module names have precedence over identifier declarations

check explicit module names for conformity

list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors

support indirect corecursion

tuned proofs;

tuned proofs;

tuned proofs;

tuned;

tuned proofs;

interpret keys more movement only when needed;

non-persistent print_state: trade-off between JVM space vs. ML time;

some explicit indication of Proof General legacy;

merge

various refactoring; handle self-mappings; handle range types containing function types;

expose basic Symbol.properties (uninterpreted);

tuned proofs;

remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list); handle KP_UP/KP_DOWN keys as well, like Swing does;

no completion on backspace -- too intrusive, e.g. when deleting keywords;

more contributors;