simplified interface for ML antiquotations, struct_name is always "Isabelle";

tuned isatest ML_OPTIONS;

removed ever experimental support for Moscow ML -- hardly works anymore;

result: Single_Assignment.var;

removed slightly adhoc single-assignment feature, cf. structure Single_Assignment; access: uninterruptible update/broadcast, to prevent lost signals;

explicit representation of single-assignment variables;

fixed spelling;

removed unused "boundary" of Table/Graph.get_first;

proper treatment of paths passed to the shell -- to allow spaces in file names as usual;

renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;

misc tuning;

merged

adjusted to changeset 118b41bba42b5

tuned font handling; explicit workaround for Apple's font manager in Java 1.6, which fails to create "IsabelleTextBold" as family member of "IsabelleText";

updated versions of requirements;

filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);

eliminated self intersection and non-integer coordinates;

try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;

updated generated files;

merged

Changed 'bounded unique existential quantifiers' from a constant to syntax translation.

four changes to Nitpick: 1. avoid writing absolute paths in Kodkodi files for input/output files of external SAT solvers (e.g. MiniSat), to dodge Cygwin problems 2. do eta-contraction in the monotonicity check 3. improved quantifier massaging algorithms using ideas from Paradox 4. repaired "check_potential" and "check_genuine"

capture error messages (of SMT solvers)

updated dependencies

merged

updated SMT certificates

updated examples due to changes in the way SMT certificates are stored

merged

merged

Adapted to changes in cases method.

Adapted to changes in setup of cases method.

Added setup for simplification of equality constraints in cases rules.

Added infrastructure for simplifying equality constraints in cases rules.

Added "constraints" tag / attribute for specifying the number of equality constraints in cases rules.

updated SMT certificates

updated SMT examples

collect certificates in a single file

added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick

Removed explicit type annotations

adjusted to changes in List_Set.thy

more correspondence lemmas between related operations

canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply

dropped some redundancies

generalized lemma foldl_apply_inv to foldl_apply

more correspondence lemmas between related operations; tuned some proofs

new theory Algebras.thy for generic algebraic structures

dropped mk_left_commute; use interpretation of locale abel_semigroup instead

merged

a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML

lemma Image_closed_trancl

corrected type of typecopy constructor

tuned structure; moved non-related quickcheck.setup to Code_Generator.thy

Changed author; removed debugging code.

merged

adding Mutabelle to repository

Replaced vec1 and dest_vec1 by abbreviation.

merged

HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)

merged

support skolem constant for extensional arrays in Z3 proofs

drop underscores at end of names coming from Boogie

merged

correctly hiding facts of Lazy_Sequence

corrected and simplified Spec_Rules registration in the Recdef package