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
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
2011-06-23, by wenzelm
clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
2011-06-23, by wenzelm
more robust concurrent builds;
2011-06-23, by wenzelm
merged
2011-06-23, by huffman
add countable_datatype method for proving countable class instances
2011-06-23, by huffman
merged;
2011-06-23, by wenzelm
instance inat :: number_semiring
2011-06-23, by huffman
added number_semiring class, plus a few new lemmas;
2011-06-23, by huffman
merged
2011-06-23, by blanchet
fiddle with remote ATP settings, based on Judgment Day
2011-06-23, by blanchet
give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers
2011-06-23, by blanchet
Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
2011-06-23, by ballarin
generalize lemmas power_number_of_even and power_number_of_odd
2011-06-22, by huffman
merged
2011-06-22, by huffman
add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
2011-06-22, by huffman
simplified arrangement of jars;
2011-06-23, by wenzelm
adapted to Cygwin;
2011-06-23, by wenzelm
provide Isabelle/Scala environment as Java extension, instead of user classpath
2011-06-23, by wenzelm
explicit import java.lang.System to prevent odd scope problems;
2011-06-23, by wenzelm
ensure export of initial CLASSPATH;
2011-06-23, by wenzelm
augment Java extension directories;
2011-06-23, by wenzelm
basic setup for Isabelle charset;
2011-06-23, by wenzelm
prefer actual charset over charset name;
2011-06-22, by wenzelm
clarified default ML settings;
2011-06-22, by wenzelm
lazy Isabelle_System.default supports implicit boot;
2011-06-22, by wenzelm
clarified plugin start/stop;
2011-06-22, by wenzelm
clarified init/exit procedure;
2011-06-22, by wenzelm
clarified decoded control symbols;
2011-06-22, by wenzelm
init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
2011-06-22, by wenzelm
prefer STIXGeneral -- hard to tell if better or worse;
2011-06-22, by wenzelm
merged
2011-06-22, by wenzelm
export lambda-lifting code as there is potential use for it within Sledgehammer
2011-06-22, by boehmes
updated to jedit-4.4.1 and jedit_build-20110622;
2011-06-22, by wenzelm
clarified chunk.offset, chunk.length;
2011-06-22, by wenzelm
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
2011-06-21, by wenzelm
some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;
2011-06-21, by wenzelm
more precise font transformations: shift sub/superscript, adjust size for user fonts;
2011-06-21, by wenzelm
don't change the way helpers are generated for the exporter's sake
2011-06-21, by blanchet
provide appropriate type system and number of fact defaults for remote ATPs
2011-06-21, by blanchet
order generated facts topologically
2011-06-21, by blanchet
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
2011-06-21, by blanchet
tweaked E, SPASS, Vampire setup based on latest Judgment Day results
2011-06-21, by blanchet
remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
2011-06-21, by blanchet
avoid double ASCII-fication
2011-06-21, by blanchet
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
2011-06-21, by blanchet
generate type predicates for existentials/skolems, otherwise some problems might not be provable
2011-06-21, by blanchet
insert rather than append special facts to make it less likely that they're truncated away
2011-06-21, by blanchet
hidden font: full height makes cursor more visible;
2011-06-21, by wenzelm
more uniform treatment of recode_set/recode_map;
2011-06-21, by wenzelm
tuned iteration over short symbols;
2011-06-21, by wenzelm
Symbol.is_ctrl: handle decoded version as well;
2011-06-21, by wenzelm
some support for user symbol fonts;
2011-06-21, by wenzelm
removed obsolete font specification;
2011-06-20, by wenzelm
more tolerant Symbol.decode;
2011-06-20, by wenzelm
simplified/generalized ISABELLE_FONTS handling;
2011-06-20, by wenzelm
updated to jedit_build-20110620;
2011-06-20, by wenzelm
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
2011-06-20, by wenzelm
clean up SPASS FLOTTER hack
2011-06-20, by blanchet
remove automatic recovery from (some) unsound proofs, now that we use sound encodings for all the interesting provers
2011-06-20, by blanchet
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
2011-06-20, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip