tuned spelling

tuned proofs

hide fact Nat.add_0_right; make add_0_right from Groups priority

tuned header

using code antiquotation

tuned header

dropped accidental duplication of "lin" prefix from cs. 108662d50512

NEWS: ax_simps

avoid upto in generated code (is infix operator in library.ML)

separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4

merged

more precise proofs

moved auxiliary lemmas to more appropriate places

separate library theory for type classes combining lattices with various algebraic structures; more simp rules

dropped instantiations for combined lattices

added lemmas involving Min, Max, uminus

tuned proof

separate library theory for type classes combining lattices with various algebraic structures

more quotes;

merged

separate theory for index structures

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS

added explaining comment; added ac_simps slot; drop unused abstract lattice; dropped mysterious syntax declaration

split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts, modernized perl scripts: prefer standalone executables

removed paranoia setting of signal handler -- appears to be no longer necessary (thanks to Cygwin 1.7?);

modernized perl scripts: prefer standalone executables; exec bash wrapper script directly -- avoid intermediate process;

modernized perl scripts: prefer standalone executables;

renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;

prefer explicit @{lemma} over adhoc forward reasoning;

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.