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

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
slightly better setup for E
2011-06-20, by blanchet
respect "really_all" argument, which is used by "ATP_Export"
2011-06-20, by blanchet
slightly better setup for SPASS and Vampire as more results have come in
2011-06-20, by blanchet
optimized SPASS and Vampire time slices, like E before
2011-06-20, by blanchet
optimized E's time slicing, based on latest exhaustive Judgment Day results
2011-06-20, by blanchet
deal with ATP time slices in a more flexible/robust fashion
2011-06-20, by blanchet
literal unicode in README.html allows to copy/paste from Lobo output;
2011-06-20, by wenzelm
merged;
2011-06-19, by wenzelm
explain special control symbols;
2011-06-19, by wenzelm
accept control symbols;
2011-06-19, by wenzelm
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
2011-06-19, by blanchet
recognize one more E failure message
2011-06-19, by blanchet

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

isabelle