Mercurialisabelle / shortlog
summary | shortlog | changelog | graph | tags | branches | files | gz
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip
 
2010-02-08 huffman 2010-02-08 merged changeset | files
2010-02-08 huffman 2010-02-08 correct definedness side conditions for copy_apps and take_apps changeset | files
2010-02-08 huffman 2010-02-08 handle case where copy_stricts cannot be proven; rewrite proof script for take_apps changeset | files
2010-02-07 huffman 2010-02-07 rewrite proof script for take_stricts changeset | files
2010-02-07 huffman 2010-02-07 remove redundant theorem attributes changeset | files
2010-02-07 huffman 2010-02-07 add lemma iterate_below_fix changeset | files
2010-02-08 wenzelm 2010-02-08 modernized some syntax translations; changeset | files
2010-02-08 wenzelm 2010-02-08 more precise dependencies; changeset | files
2010-02-08 haftmann 2010-02-08 merged changeset | files
2010-02-08 haftmann 2010-02-08 re-generated certificates changeset | files
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields changeset | files
2010-02-08 haftmann 2010-02-08 tuned spelling changeset | files
2010-02-08 haftmann 2010-02-08 tuned proofs changeset | files
2010-02-08 haftmann 2010-02-08 hide fact Nat.add_0_right; make add_0_right from Groups priority changeset | files
2010-02-08 haftmann 2010-02-08 tuned header changeset | files
2010-02-08 haftmann 2010-02-08 using code antiquotation changeset | files
2010-02-08 haftmann 2010-02-08 tuned header changeset | files
2010-02-08 haftmann 2010-02-08 dropped accidental duplication of "lin" prefix from cs. 108662d50512 changeset | files
2010-02-08 haftmann 2010-02-08 NEWS: ax_simps changeset | files
2010-02-08 haftmann 2010-02-08 avoid upto in generated code (is infix operator in library.ML) changeset | files
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4 changeset | files
2010-02-08 haftmann 2010-02-08 merged changeset | files
2010-02-08 haftmann 2010-02-08 more precise proofs changeset | files
2010-02-08 haftmann 2010-02-08 moved auxiliary lemmas to more appropriate places changeset | files
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures; more simp rules changeset | files
2010-02-08 haftmann 2010-02-08 dropped instantiations for combined lattices changeset | files
2010-02-08 haftmann 2010-02-08 added lemmas involving Min, Max, uminus changeset | files
2010-02-08 haftmann 2010-02-08 tuned proof changeset | files
2010-02-08 haftmann 2010-02-08 separate library theory for type classes combining lattices with various algebraic structures changeset | files
2010-02-08 wenzelm 2010-02-08 more quotes; changeset | files
2010-02-08 haftmann 2010-02-08 merged changeset | files
2010-02-08 haftmann 2010-02-08 separate theory for index structures changeset | files
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS changeset | files
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS changeset | files
2010-02-05 haftmann 2010-02-05 added explaining comment; added ac_simps slot; drop unused abstract lattice; dropped mysterious syntax declaration changeset | files
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 changeset | files
2010-02-07 wenzelm 2010-02-07 removed paranoia setting of signal handler -- appears to be no longer necessary (thanks to Cygwin 1.7?); changeset | files
2010-02-07 wenzelm 2010-02-07 modernized perl scripts: prefer standalone executables; exec bash wrapper script directly -- avoid intermediate process; changeset | files
2010-02-07 wenzelm 2010-02-07 modernized perl scripts: prefer standalone executables; changeset | files
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; changeset | files
2010-02-07 wenzelm 2010-02-07 prefer explicit @{lemma} over adhoc forward reasoning; changeset | files
2010-02-07 wenzelm 2010-02-07 simplified interface for ML antiquotations, struct_name is always "Isabelle"; changeset | files
2010-02-06 wenzelm 2010-02-06 tuned isatest ML_OPTIONS; changeset | files
2010-02-06 wenzelm 2010-02-06 removed ever experimental support for Moscow ML -- hardly works anymore; changeset | files
2010-02-06 wenzelm 2010-02-06 result: Single_Assignment.var; changeset | files
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; changeset | files
2010-02-06 wenzelm 2010-02-06 explicit representation of single-assignment variables; changeset | files
2010-02-06 wenzelm 2010-02-06 fixed spelling; changeset | files
2010-02-06 wenzelm 2010-02-06 removed unused "boundary" of Table/Graph.get_first; changeset | files
2010-02-06 wenzelm 2010-02-06 proper treatment of paths passed to the shell -- to allow spaces in file names as usual; changeset | files
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; changeset | files
2010-02-06 wenzelm 2010-02-06 misc tuning; changeset | files
2010-02-06 haftmann 2010-02-06 merged changeset | files
2010-02-06 haftmann 2010-02-06 adjusted to changeset 118b41bba42b5 changeset | files
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"; changeset | files
2010-02-05 wenzelm 2010-02-05 updated versions of requirements; changeset | files
2010-02-05 wenzelm 2010-02-05 filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>); changeset | files
2010-02-05 wenzelm 2010-02-05 eliminated self intersection and non-integer coordinates; changeset | files
2010-02-05 wenzelm 2010-02-05 try "GTK+" as well -- note that "Nimbus" is unavailable in versions of OpenJDK; changeset | files
2010-02-05 wenzelm 2010-02-05 updated generated files; changeset | files
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip
isabelle