Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-56
+56
+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.
type classes: entity markup instead of old-style token markup;
2011-06-25, by wenzelm
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-06-25, by wenzelm
clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example;
2011-06-25, by wenzelm
produce string constant directly;
2011-06-25, by wenzelm
merged
2011-06-25, by wenzelm
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
2011-06-25, by ballarin
removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;
2011-06-25, by wenzelm
clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);
2011-06-25, by wenzelm
CLASSPATH already converted in isabelle java wrapper;
2011-06-25, by wenzelm
removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;
2011-06-25, by wenzelm
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
less
more
|
(0)
-30000
-10000
-3000
-1000
-300
-100
-56
+56
+100
+300
+1000
+3000
+10000
+30000
tip