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;