| Sat, 11 Jun 2011 16:05:17 +0200 |
wenzelm |
cover method "deepen" concisely;
|
changeset |
files
|
| Sat, 11 Jun 2011 15:36:46 +0200 |
wenzelm |
moved/updated single-step tactics;
|
changeset |
files
|
| Sat, 11 Jun 2011 15:03:31 +0200 |
wenzelm |
tuned sections;
|
changeset |
files
|
| Sat, 11 Jun 2011 14:27:23 +0200 |
wenzelm |
reverted 5fcd0ca1f582 -- isatest provides its own libgmp3 via LD_LIBRARY_PATH, which are also required for swipl;
|
changeset |
files
|
| Sat, 11 Jun 2011 07:50:28 +0200 |
haftmann |
tuned comment
|
changeset |
files
|
| Fri, 10 Jun 2011 17:52:09 +0200 |
blanchet |
name tuning
|
changeset |
files
|
| Fri, 10 Jun 2011 17:52:09 +0200 |
blanchet |
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
|
changeset |
files
|
| Fri, 10 Jun 2011 17:52:09 +0200 |
blanchet |
don't trim proofs in debug mode
|
changeset |
files
|
| Fri, 10 Jun 2011 17:52:09 +0200 |
blanchet |
tuning
|
changeset |
files
|
| Fri, 10 Jun 2011 17:37:50 +0200 |
wenzelm |
isatest/makedist: build Isabelle/jEdit;
|
changeset |
files
|
| Fri, 10 Jun 2011 17:30:23 +0200 |
wenzelm |
makedist -j: build Isabelle/jEdit via given jedit_build component;
|
changeset |
files
|
| Fri, 10 Jun 2011 15:42:21 +0200 |
bulwahn |
adding another narrowing strategy for integers
|
changeset |
files
|
| Fri, 10 Jun 2011 15:03:29 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 10 Jun 2011 12:01:15 +0200 |
blanchet |
pass --trim option to "eproof" script to speed up proof reconstruction
|
changeset |
files
|
| Fri, 10 Jun 2011 12:01:15 +0200 |
blanchet |
removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them
|
changeset |
files
|
| Fri, 10 Jun 2011 12:01:15 +0200 |
blanchet |
fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day
|
changeset |
files
|
| Fri, 10 Jun 2011 12:01:15 +0200 |
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
|
changeset |
files
|
| Fri, 10 Jun 2011 14:59:30 +0200 |
wenzelm |
use existing ghc on macbroy20;
|
changeset |
files
|
| Fri, 10 Jun 2011 13:32:51 +0200 |
wenzelm |
local gensym based on Name.variant;
|
changeset |
files
|
| Fri, 10 Jun 2011 12:51:29 +0200 |
wenzelm |
uniform use of flexflex_rule;
|
changeset |
files
|
| Fri, 10 Jun 2011 11:47:52 +0200 |
wenzelm |
tuned name (cf. blast_stats);
|
changeset |
files
|
| Fri, 10 Jun 2011 11:39:23 +0200 |
wenzelm |
more official options blast_trace, blast_stats;
|
changeset |
files
|
| Thu, 09 Jun 2011 23:30:18 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 09 Jun 2011 15:14:21 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Thu, 09 Jun 2011 14:16:12 +0200 |
bulwahn |
resolving an issue with class instances that are pseudo functions in the OCaml code serializer
|
changeset |
files
|
| Thu, 09 Jun 2011 14:24:34 +0200 |
hoelzl |
merged
|
changeset |
files
|
| Thu, 09 Jun 2011 14:04:38 +0200 |
hoelzl |
fixed document generation for HOL
|
changeset |
files
|
| Thu, 09 Jun 2011 14:04:34 +0200 |
hoelzl |
lemma: independence is equal to mutual information = 0
|
changeset |
files
|
| Thu, 09 Jun 2011 13:55:11 +0200 |
hoelzl |
jensens inequality
|
changeset |
files
|
| Thu, 09 Jun 2011 11:50:16 +0200 |
hoelzl |
lemmas about right derivative and limits
|
changeset |
files
|
| Thu, 09 Jun 2011 11:50:16 +0200 |
hoelzl |
lemma about differences of convex functions
|
changeset |
files
|
| Thu, 09 Jun 2011 11:50:16 +0200 |
hoelzl |
lemmas relating ln x and x - 1
|
changeset |
files
|