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;

updated TPTP parser to conform to version 5.5.0 (but excluding the TPI language since its parser spec is still incomplete);

updated TPTP parser to conform to version 5.4.0; clarified abstract syntax for 'let' in TPTP_Syntax (and in the parser); improved parsing of 'let' (in TFF) -- previously it wasn't looking at the structure of the definition; fixed bug when parsing 'let' (in TFF and THF) -- was only keeping the first quantified variable, and ignoring the rest; added comments to remind that 'let' support for THF is currently broken in TPTP;

included axiom formulas (removing a FIXME) in the imported problem; turned tests into asserts; changed problem to one which actually succeeds using z3;

updated syntax to use 'ML_file' rather than 'uses';

now allowing numeric identifiers to be used in 'file' annotations; more informative failure of missed cases by raising ANNOT_STRUCTURE instead of the default Match;

get_file_list now returns files sorted by size;

brought up to date with TPTP_Proof;