2011-10-12 ago wenzelm modernized structure Induct_Tacs;
2011-10-12 ago wenzelm tuned signature;
2011-10-12 ago wenzelm misc tuning and clarification;
2011-10-12 ago wenzelm tuned ML style;
2011-10-12 ago wenzelm tuned proofs -- eliminated vacuous "induct arbitrary: ..." situations;
2011-10-12 ago wenzelm discontinued obsolete alias structure ProofContext;
2011-10-12 ago nipkow separated monotonicity reasoning and defined narrowing with while_option
2011-10-10 ago wenzelm include no-smlnj targets into library (cf. e54a985daa61);
2011-10-10 ago bulwahn increasing values_timeout to avoid SML_makeall failures on our current tests
2011-10-10 ago wenzelm merged
2011-10-10 ago wenzelm removed obsolete RC tags;
2011-10-09 ago huffman Int.thy: discontinued some legacy theorems
2011-10-09 ago huffman Set.thy: remove redundant [simp] declarations
2011-10-03 ago bulwahn removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
2011-10-03 ago bulwahn tune text for document generation
2011-10-03 ago bulwahn adding examples with relations to Quickcheck_Examples to show that quickcheck can actually handle operators on relations as well
2011-10-03 ago bulwahn adding code equations for cardinality and (reflexive) transitive closure on finite types
2011-10-03 ago bulwahn adding lemma about rel_pow in Transitive_Closure for executable equation of the (refl) transitive closure
2011-10-03 ago bulwahn adding lemma to List library for executable equation of the (refl) transitive closure
2011-09-29 ago Jean Pichon fixed typos in IMP
2011-09-28 ago nipkow added nice interval syntax
2011-09-28 ago nipkow Added dependecies
2011-09-28 ago nipkow Added Hoare-like Abstract Interpretation
2011-09-28 ago nipkow moved IMP/AbsInt stuff into subdirectory Abs_Int_Den
2011-09-26 ago wenzelm back to post-release mode;
2011-10-09 ago wenzelm Added tag Isabelle2011-1 for changeset 76fef3e57004
2011-10-09 ago wenzelm tuned; Isabelle2011-1
2011-10-09 ago wenzelm updated ISABELLE_HOME_USER;
2011-10-04 ago wenzelm more explicit check of Java executable -- relevant for Linux x86/x86_64 mismatch and absence on Mac OS Lion;
2011-10-03 ago wenzelm Added tag Isabelle2011-1-RC2 for changeset a45121ffcfcb
2011-10-03 ago wenzelm some amendments due to Jean Pichon;
2011-09-29 ago traytel correct coercion generation in case of unknown map functions
2011-09-28 ago wenzelm proper platform_file_url for Windows UNC paths (server shares);
2011-09-27 ago wenzelm proper platform_file_url;
2011-09-27 ago wenzelm observe base URL of rendered document;
2011-09-27 ago wenzelm more README;
2011-09-27 ago wenzelm tuned README.html;
2011-09-27 ago wenzelm tuned;
2011-09-27 ago wenzelm retain output, which is required for non-existent JRE, for example (cf. b455e4f42c04);
2011-09-27 ago wenzelm tuned message, which is displayed after termination of Isabelle.app on Mac OS;
2011-09-26 ago wenzelm keep top-level "Isabelle" executable -- now an alias for "isabelle jedit";
2011-09-26 ago wenzelm tuned;
2011-09-26 ago wenzelm ensure Isabelle env;
2011-09-26 ago wenzelm Added tag Isabelle2011-1-RC1 for changeset 24ad77c3a147
2011-09-26 ago wenzelm tuned;
2011-09-26 ago wenzelm misc tuning for release;
2011-09-26 ago wenzelm reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
2011-09-26 ago wenzelm makedist for release;
2011-09-26 ago blanchet put MiniSat back first -- Torlak's eval seemed to suggest that Crypto and Lingeling were better, but Crypto is slower on "Nitpick_Examples" and Crypto crashes
2011-09-26 ago blanchet require Java 1.6 in the Nitpick documentation -- technically 1.5 will also work with Kodkodi 1.2.16, but it won't work with Kodkodi 1.5.0
2011-09-26 ago blanchet put CryptoMiniSat first and remove warning about unsoundness now that it has been fixed in Kodkod
2011-09-26 ago bulwahn adding an example with inductive predicates to quickcheck narrowing examples
2011-09-26 ago bulwahn importing the Generated_Code module qualified to reduce the probability of name clashes between the static code and the generated code in the narrowing-based Quickcheck
2011-09-25 ago blanchet clarify platforms
2011-09-25 ago blanchet killed JNI version of zChaff, since Kodkod 1.5 does not support it anymore
2011-09-25 ago blanchet updated Nitpick SAT Solver doc
2011-09-25 ago blanchet update list of SAT solvers reflecting Kodkod 1.5
2011-09-25 ago wenzelm tuned signature;
2011-09-25 ago wenzelm more uniform defaults;
2011-09-25 ago haftmann Quotient_Set.thy is part of library