refactoring -- splitting between constructor sugar dependencies and true BNF dependencies

renamed ML files

renamed theory file

tuned signature -- facilitate experimentation with other processes;

preserve types during rewriting

made SML/NJ happy

made SML/NJ happy

made SML/NJ happier

added experimental configuration options to tune use of builtin symbols in SMT

added possibility to reset builtins (for experimentation)

just one data slot (record) per program unit

more "primrec_new" documentation

merged

tuned signature;

eliminated clone of Inductive.mk_cases_tac;

tuned signature;

tuned whitespace;

provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);

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);