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

tuned

removed dead code

keep a database of free constructor type information

generalized case-handling code a bit

support cases for new-style (co)datatypes

use case rather than sequence of ifs in expansion

textual improvements following Christian Sternagel's feedback

generalize lemma

removed unused lemma

factor out new lemma

replace lemma with more general simp rule

generalized tactics

renamed generated property

commented out debugging output in "primcorec"

merged

tuned proofs;

more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);

NEWS;

clarified font;

simplified default L&F -- Nimbus should be always available and GTK+ is not fully working yet;

proper platform-specific test;

disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;

focus text field, to capture key events even on Mac OS X look-and-feel;

tuned proofs;

more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;