isabelle: Graph

removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
2011-06-27, by blanchet
clarify warning message to avoid confusing beginners
2011-06-27, by blanchet
remove experimental trimming feature -- it slowed down things on Linux for some reason
2011-06-27, by blanchet
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
2011-06-27, by blanchet
NEWS;
2011-06-27, by wenzelm
document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27, by wenzelm
proper checking of @{ML_antiquotation};
2011-06-27, by wenzelm
hide rather short auxiliary names, which can easily occur in user theories;
2011-06-27, by wenzelm
updated generated file;
2011-06-27, by wenzelm
ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27, by wenzelm
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-27, by wenzelm
parallel Syntax.parse, which is rather slow;
2011-06-27, by wenzelm
markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
2011-06-27, by wenzelm
move conditional expectation to its own theory file
2011-06-27, by hoelzl
updated SMT certificates
2011-06-26, by boehmes
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
2011-06-26, by boehmes
proper tokens only if session is ready;
2011-06-25, by wenzelm
entity markup for "type", "constant";
2011-06-25, by wenzelm
clarified Markup.CLASS vs. HTML.CLASS;
2011-06-25, by wenzelm
tuned color, to avoid confusion with type variables;
2011-06-25, by wenzelm
discontinued generic XML markup -- this is for XHTML with <span/> elements;
2011-06-25, by wenzelm
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
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
tweaked TPTP formula kind for typing information used in the conjecture
2011-06-19, by blanchet
more forceful message
2011-06-19, by blanchet
treat quotes as non-controllable, to reduce surprise in incremental editing;
2011-06-19, by wenzelm
abbreviations for special control symbols;
2011-06-19, by wenzelm
completion for control symbols;
2011-06-19, by wenzelm
updated to jedit_build-20110619;
2011-06-19, by wenzelm
support for bold style within text buffer;
2011-06-19, by wenzelm
tuned;
2011-06-19, by wenzelm
discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);
2011-06-19, by wenzelm