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