2013-09-29 wenzelm 2013-09-29 updated to sumatra_pdf-2.3.2;
2013-09-29 wenzelm 2013-09-29 low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
2013-09-29 wenzelm 2013-09-29 backout c6297fa1031a -- strange parsers are required to make this work;
2013-09-28 wenzelm 2013-09-28 make SML/NJ more happy;
2013-09-28 wenzelm 2013-09-28 enforce IsabelleText font for better symbol coverage, especially on Windows;
2013-09-28 wenzelm 2013-09-28 proper wrapper for parser -- more explicit error;
2013-09-28 wenzelm 2013-09-28 misc tuning for release;
2013-09-28 wenzelm 2013-09-28 remove remains from WinRun4J;
2013-09-28 wenzelm 2013-09-28 proper document markup;
2013-09-28 wenzelm 2013-09-28 uniform $ISABELLE_HOME on all platforms;
2013-09-28 wenzelm 2013-09-28 simplified ISABELLE_HOME on Windows (see also 9c8a1b9c0630, 5a7903ba2dac);
2013-09-28 wenzelm 2013-09-28 update second environment that is used for System.getenv(String);
2013-09-28 wenzelm 2013-09-28 adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
2013-09-27 kuncar 2013-09-27 tuned names
2013-09-27 kuncar 2013-09-27 fold and lemmas about cardinality
2013-09-27 wenzelm 2013-09-27 more robust parser: 'imports' are mandatory except for bootstrapping Pure;
2013-09-27 blanchet 2013-09-27 one more unfolding necessary
2013-09-27 blanchet 2013-09-27 faster exit in common case
2013-09-27 nipkow 2013-09-27 merged
2013-09-27 nipkow 2013-09-27 hide coercion
2013-09-27 blanchet 2013-09-27 fixed one line that would never have compiled in a typed language + release the lock in case of exceptions
2013-09-27 nipkow 2013-09-27 merged
2013-09-27 nipkow 2013-09-27 added Bleast code eqns for RBT
2013-09-27 nipkow 2013-09-27 added code eqns for bounded LEAST operator
2013-09-27 kuncar 2013-09-27 new theory of finite sets as a subtype
2013-09-27 kuncar 2013-09-27 new parametricity rules and useful lemmas
2013-09-27 kuncar 2013-09-27 allow to specify multiple parametricity transfer rules in lift_definition
2013-09-27 Andreas Lochbihler 2013-09-27 merged
2013-09-27 Andreas Lochbihler 2013-09-27 generalise lemma
2013-09-27 wenzelm 2013-09-27 proper latex;
2013-09-27 Andreas Lochbihler 2013-09-27 merged
2013-09-27 Andreas Lochbihler 2013-09-27 add relator for 'a filter and parametricity theorems
2013-09-27 Andreas Lochbihler 2013-09-27 tuned proofs
2013-09-27 Andreas Lochbihler 2013-09-27 add lemmas
2013-09-27 Andreas Lochbihler 2013-09-27 prefer Code.abort over code_abort
2013-09-27 lammich 2013-09-27 merged
2013-09-26 lammich 2013-09-26 Added Item_Net.retrieve_matching
2013-09-26 lammich 2013-09-26 Added symmetric code_unfold-lemmas for null and is_none
2013-09-26 huffman 2013-09-26 tuned proofs
2013-09-26 huffman 2013-09-26 moved lemma
2013-09-26 wenzelm 2013-09-26 merged
2013-09-26 wenzelm 2013-09-26 proper regexp;
2013-09-26 wenzelm 2013-09-26 added Isabelle/ML example;
2013-09-26 wenzelm 2013-09-26 updated jedit.jar, jEdit-patched.tar.gz according to 239f8f451976;
2013-09-26 wenzelm 2013-09-26 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);
2013-09-26 wenzelm 2013-09-26 more uniform modes (NB: comments etc. are handled by isabelle.Token_Markup.Marker);
2013-09-26 wenzelm 2013-09-26 support more brackets (see also 427724cff970, 7bf637b65ba2);
2013-09-26 huffman 2013-09-26 tuned proofs
2013-09-26 blanchet 2013-09-26 further strengthening of tactics
2013-09-26 Andreas Lochbihler 2013-09-26 merged
2013-09-26 Andreas Lochbihler 2013-09-26 add lemmas
2013-09-26 blanchet 2013-09-26 strengthened tactic
2013-09-26 blanchet 2013-09-26 tuning
2013-09-26 blanchet 2013-09-26 avoid calls to nth with ~1
2013-09-26 blanchet 2013-09-26 tuning
2013-09-26 blanchet 2013-09-26 strengthened tactic
2013-09-26 blanchet 2013-09-26 tactic cleanup
2013-09-26 blanchet 2013-09-26 made tactic more robust in case somebody specified a discriminator for a one-constructor type
2013-09-26 blanchet 2013-09-26 tuning
2013-09-26 blanchet 2013-09-26 use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity