isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

reverted 5fcd0ca1f582 -- isatest provides its own libgmp3 via LD_LIBRARY_PATH, which are also required for swipl;
2011-06-11, by wenzelm
tuned comment
2011-06-11, by haftmann
name tuning
2011-06-10, by blanchet
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
2011-06-10, by blanchet
don't trim proofs in debug mode
2011-06-10, by blanchet
tuning
2011-06-10, by blanchet
isatest/makedist: build Isabelle/jEdit;
2011-06-10, by wenzelm
makedist -j: build Isabelle/jEdit via given jedit_build component;
2011-06-10, by wenzelm
adding another narrowing strategy for integers
2011-06-10, by bulwahn
merged
2011-06-10, by wenzelm
pass --trim option to "eproof" script to speed up proof reconstruction
2011-06-10, by blanchet
removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them
2011-06-10, by blanchet
fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day
2011-06-10, by blanchet
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
2011-06-10, by blanchet
use existing ghc on macbroy20;
2011-06-10, by wenzelm
local gensym based on Name.variant;
2011-06-10, by wenzelm
uniform use of flexflex_rule;
2011-06-10, by wenzelm
tuned name (cf. blast_stats);
2011-06-10, by wenzelm
more official options blast_trace, blast_stats;
2011-06-10, by wenzelm
merged
2011-06-09, by wenzelm
merged
2011-06-09, by bulwahn
resolving an issue with class instances that are pseudo functions in the OCaml code serializer
2011-06-09, by bulwahn
merged
2011-06-09, by hoelzl
fixed document generation for HOL
2011-06-09, by hoelzl
lemma: independence is equal to mutual information = 0
2011-06-09, by hoelzl
jensens inequality
2011-06-09, by hoelzl
lemmas about right derivative and limits
2011-06-09, by hoelzl
lemma about differences of convex functions
2011-06-09, by hoelzl
lemmas relating ln x and x - 1
2011-06-09, by hoelzl
use divide instead of inverse for the derivative of ln
2011-05-31, by hoelzl
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
2011-06-09, by bulwahn
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09, by wenzelm
document depth arguments of method "auto";
2011-06-09, by wenzelm
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
2011-06-09, by wenzelm
clarified special incr_type_indexes;
2011-06-09, by wenzelm
tuned signature: Name.invent and Name.invent_names;
2011-06-09, by wenzelm
modernized structure ProofContext;
2011-06-08, by wenzelm
even more robust \isaspacing;
2011-06-09, by wenzelm
simplified Name.variant -- discontinued builtin fold_map;
2011-06-09, by wenzelm
some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);
2011-06-09, by wenzelm
discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-09, by wenzelm
prefer new-style Name.invents;
2011-06-09, by wenzelm
more tight name invention -- avoiding old functions;
2011-06-09, by wenzelm
\frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;
2011-06-09, by wenzelm
tuned;
2011-06-09, by wenzelm
NEWS
2011-06-09, by bulwahn
correcting import theory of examples
2011-06-09, by bulwahn
fixing code generation test
2011-06-09, by bulwahn
removing char setup
2011-06-09, by bulwahn
removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
2011-06-09, by bulwahn
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
2011-06-09, by bulwahn
adding narrowing engine for existentials
2011-06-09, by bulwahn
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
2011-06-09, by bulwahn
adding theory Quickcheck_Narrowing to HOL-Main image
2011-06-09, by bulwahn
adapting IsaMakefile
2011-06-09, by bulwahn
moving Quickcheck_Narrowing from Library to base directory
2011-06-09, by bulwahn
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
2011-06-09, by bulwahn
local simp rule in List_Cset
2011-06-09, by bulwahn
tuning
2011-06-09, by blanchet
compile
2011-06-09, by blanchet

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle