2010-02-08 haftmann 2010-02-08 tuned header
2010-02-08 haftmann 2010-02-08 using code antiquotation
2010-02-08 haftmann 2010-02-08 tuned header
2010-02-08 haftmann 2010-02-08 dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-08 haftmann 2010-02-08 NEWS: ax_simps
2010-02-08 haftmann 2010-02-08 avoid upto in generated code (is infix operator in library.ML)
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 more precise proofs
2010-02-08 haftmann 2010-02-08 moved auxiliary lemmas to more appropriate places
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures; more simp rules
2010-02-08 haftmann 2010-02-08 dropped instantiations for combined lattices
2010-02-08 haftmann 2010-02-08 added lemmas involving Min, Max, uminus
2010-02-08 haftmann 2010-02-08 tuned proof
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures
2010-02-08 wenzelm 2010-02-08 more quotes;
2010-02-08 haftmann 2010-02-08 merged
2010-02-08 haftmann 2010-02-08 separate theory for index structures
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-05 haftmann 2010-02-05 added explaining comment; added ac_simps slot; drop unused abstract lattice; dropped mysterious syntax declaration
2010-02-08 boehmes 2010-02-08 split SMT perl script: certificate caching and invokation of remote solvers are now in separate scripts, modernized perl scripts: prefer standalone executables
2010-02-07 wenzelm 2010-02-07 removed paranoia setting of signal handler -- appears to be no longer necessary (thanks to Cygwin 1.7?);
2010-02-07 wenzelm 2010-02-07 modernized perl scripts: prefer standalone executables; exec bash wrapper script directly -- avoid intermediate process;
2010-02-07 wenzelm 2010-02-07 modernized perl scripts: prefer standalone executables;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-02-07 wenzelm 2010-02-07 prefer explicit @{lemma} over adhoc forward reasoning;
2010-02-07 wenzelm 2010-02-07 simplified interface for ML antiquotations, struct_name is always "Isabelle";
2010-02-06 wenzelm 2010-02-06 tuned isatest ML_OPTIONS;
2010-02-06 wenzelm 2010-02-06 removed ever experimental support for Moscow ML -- hardly works anymore;
2010-02-06 wenzelm 2010-02-06 result: Single_Assignment.var;
2010-02-06 wenzelm 2010-02-06 removed slightly adhoc single-assignment feature, cf. structure Single_Assignment; access: uninterruptible update/broadcast, to prevent lost signals;
2010-02-06 wenzelm 2010-02-06 explicit representation of single-assignment variables;
2010-02-06 wenzelm 2010-02-06 fixed spelling;
2010-02-06 wenzelm 2010-02-06 removed unused "boundary" of Table/Graph.get_first;
2010-02-06 wenzelm 2010-02-06 proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
2010-02-06 wenzelm 2010-02-06 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2010-02-06 wenzelm 2010-02-06 misc tuning;
2010-02-06 haftmann 2010-02-06 merged
2010-02-06 haftmann 2010-02-06 adjusted to changeset 118b41bba42b5
2010-02-06 wenzelm 2010-02-06 tuned font handling; explicit workaround for Apple's font manager in Java 1.6, which fails to create "IsabelleTextBold" as family member of "IsabelleText";
2010-02-05 wenzelm 2010-02-05 updated versions of requirements;
2010-02-05 wenzelm 2010-02-05 filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
2010-02-05 wenzelm 2010-02-05 eliminated self intersection and non-integer coordinates;
2010-02-05 wenzelm 2010-02-05 try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK;
2010-02-05 wenzelm 2010-02-05 updated generated files;
2010-02-05 wenzelm 2010-02-05 merged
2010-02-04 hoelzl 2010-02-04 Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
2010-02-04 blanchet 2010-02-04 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"
2010-02-02 boehmes 2010-02-02 capture error messages (of SMT solvers)
2010-02-02 boehmes 2010-02-02 updated dependencies
2010-02-02 boehmes 2010-02-02 merged
2010-02-02 boehmes 2010-02-02 updated SMT certificates
2010-02-02 boehmes 2010-02-02 updated examples due to changes in the way SMT certificates are stored
2010-02-02 berghofe 2010-02-02 merged
2010-01-31 berghofe 2010-01-31 merged
2010-01-30 berghofe 2010-01-30 Adapted to changes in cases method.
2010-01-30 berghofe 2010-01-30 Adapted to changes in setup of cases method.
2010-01-30 berghofe 2010-01-30 Added setup for simplification of equality constraints in cases rules.
2010-01-30 berghofe 2010-01-30 Added infrastructure for simplifying equality constraints in cases rules.