isabelle: Graph

no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
2011-05-30, by blanchet
better merging of similar outputs
2011-05-30, by blanchet
update minimization documentation
2011-05-30, by blanchet
imported patch sledge_doc_metis_as_prover
2011-05-30, by blanchet
automatically minimize with Metis when this can be done within a few seconds
2011-05-30, by blanchet
minimize with Metis if possible
2011-05-30, by blanchet
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
2011-05-30, by blanchet
Workaround for hyperref bug affecting index entries involving the | symbol
2011-05-30, by paulson
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
2011-05-30, by bulwahn
automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option
2011-05-30, by bulwahn
merged multiple heads
2011-05-30, by paulson
Fix to exception THM 1 raised (line 212 of conv.ML), reported by Andreas Lochbihler
2011-05-30, by paulson
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
2011-05-29, by blanchet
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
2011-05-29, by blanchet
function tutorial: do not omit termination proof, even when discussing other things
2011-05-27, by krauss
added re-implemented monomorphizer for types with better control for number of generated instances (strict as opposed to the SMT monomorphizer) and with fact annotations controlling in which round certain facts are considered for monomorphization
2011-05-27, by boehmes
document new "try"
2011-05-27, by blanchet
tuned comments
2011-05-27, by blanchet
new timeout section (cf. Nitpick manual)
2011-05-27, by blanchet
cleanup proof text generation code
2011-05-27, by blanchet
more Sledgehammer documentation updates
2011-05-27, by blanchet
minor update
2011-05-27, by blanchet
try both "metis" and (on failure) "metisFT" in replay
2011-05-27, by blanchet
show time taken for reconstruction
2011-05-27, by blanchet
unbreak "max_potential" logic
2011-05-27, by blanchet
more concise output
2011-05-27, by blanchet
compile
2011-05-27, by blanchet
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
2011-05-27, by blanchet
repaired theory merging and defined/used helpers
2011-05-27, by blanchet
make Sledgehammer a little bit less verbose in "try"
2011-05-27, by blanchet
handle non-auto try cases gracefully in Try Methods
2011-05-27, by blanchet
handle non-auto try case gracefully in Solve Direct
2011-05-27, by blanchet
prioritize try and auto try's tools, with fast ones first, with a slight preference for provers vs. counterexample generators
2011-05-27, by blanchet
update SML section of documentation
2011-05-27, by blanchet
handle non-auto try case gracefully in Nitpick
2011-05-27, by blanchet
handle non-auto try case of Sledgehammer better
2011-05-27, by blanchet
added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-27, by blanchet
removed FIXME: "try_methods" doesn't take a clasimpmod, because it needs to generate Isar proof text in case of success and hence needs total control over its arguments
2011-05-27, by blanchet
renamed "Auto_Tools" "Try"
2011-05-27, by blanchet
removed THF equality proxy hack now that Geoff Sutcliffe has fixed SystemOnTPTP
2011-05-27, by blanchet
renamed "try" "try_methods"
2011-05-27, by blanchet
renamed "metis_timeout" to "preplay_timeout" and continued implementation
2011-05-27, by blanchet
minor fixes to Sledgehammer docs
2011-05-27, by blanchet
shorten minimizer command further, exploiting until-now-undocumented syntax
2011-05-27, by blanchet
minor tweaks to the Nitpick documentation
2011-05-27, by blanchet
added syntax for specifying Metis timeout (currently used only by SMT solvers)
2011-05-27, by blanchet
readded Waldmeister as default to the documentation and other minor changes
2011-05-27, by blanchet
reintroduced Waldmeister but limit the number of remote threads created
2011-05-27, by blanchet
renamed "minimize" to "min" to make Sledgehammer output a little bit more concise
2011-05-27, by blanchet
minor doc adjustments
2011-05-27, by blanchet
make output more concise
2011-05-27, by blanchet
merge timeout messages from several ATPs into one message to avoid clutter
2011-05-27, by blanchet
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
2011-05-27, by blanchet
tuning
2011-05-27, by blanchet
mention contributions from LCP and explain metis and metisFT encodings
2011-05-27, by blanchet
fixed trivial fact detection
2011-05-27, by blanchet
cleaner handling of equality and proxies (esp. for THF)
2011-05-27, by blanchet
recognize more ATP failures
2011-05-27, by blanchet
fully support all type system encodings in typed formats (TFF, THF)
2011-05-27, by blanchet
take out Waldmeister from default for now -- success rate too low on Judgment Day
2011-05-27, by blanchet
document relevance filter a bit more
2011-05-27, by blanchet
always run Sledgehammer synchronously in the jEdit interface (until the multithreading support for Proof General is ported)
2011-05-27, by blanchet
towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
2011-05-27, by blanchet
instance inat for complete_lattice
2011-05-26, by noschinl
iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
2011-05-26, by boehmes
integral strong monotone; finite subadditivity for measure
2011-05-26, by hoelzl
composition of convex and measurable function is measurable
2011-05-26, by hoelzl
introduce independence of two random variables
2011-05-26, by hoelzl
add lemma indep_distribution_eq_measure
2011-05-26, by hoelzl
add lemma indep_rv_finite
2011-05-26, by hoelzl
generalize setsum_cases
2011-05-26, by hoelzl
add lemma borel_0_1_law
2011-05-26, by hoelzl
add lemma sigma_sets_singleton
2011-05-26, by hoelzl
use abbrevitation events == sets M
2011-05-26, by hoelzl
add lemma kolmogorov_0_1_law
2011-05-26, by hoelzl
add lemma indep_sets_collect_sigma
2011-05-26, by hoelzl
improving code_int setup in Quickcheck_Narrowing; adding partial_term_of class in Quickcheck_Narrowing
2011-05-26, by bulwahn
extending terms of Code_Evaluation by Free to allow partial terms
2011-05-26, by bulwahn
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command
2011-05-26, by krauss
css rules for highlighting sendback text
2011-05-26, by krauss
invert event propagation flag -- in lobobrowser api, true means re-propagate
2011-05-26, by krauss
eta-expand to make SML/NJ happy
2011-05-25, by blanchet
ensure that the argument of logical negation is enclosed in parentheses in THF mode
2011-05-24, by blanchet
hack to obtain potable step names from Waldmeister
2011-05-24, by blanchet
respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")
2011-05-24, by blanchet
further reduce the number of facts passed to less used remote ATPs
2011-05-24, by blanchet
added quietness flag
2011-05-24, by blanchet
pass fewer relevant facts to less used remote systems
2011-05-24, by blanchet
more work on parsing LEO-II proofs and extracting uses of extensionality
2011-05-24, by blanchet
tuning
2011-05-24, by blanchet
more work on parsing LEO-II proofs without lambdas
2011-05-24, by blanchet
slightly gracefuller handling of LEO-II and Satallax output
2011-05-24, by blanchet
document primitive support for LEO-II and Satallax
2011-05-24, by blanchet
identify HOL functions with THF functions
2011-05-24, by blanchet
started adding support for THF output (but no lambdas)
2011-05-24, by blanchet
eliminated more code duplication in Nitrox
2011-05-24, by blanchet
reduce code duplication in Nitrox
2011-05-24, by blanchet
use \<emdash> rather than \<midarrow>
2011-05-24, by blanchet
fixed de Bruijn index bug
2011-05-24, by blanchet
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things
2011-05-24, by blanchet
filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
2011-05-24, by blanchet
clearer SystemOnTPTP errors
2011-05-24, by blanchet
give fewer equations to Waldmeister
2011-05-24, by blanchet
detect inappropriate problems and crashes better in Waldmeister
2011-05-24, by blanchet
tuning -- the "appropriate" terminology is inspired from TPTP
2011-05-24, by blanchet
pass no type args to hAPP in "poly_args" type system, which is unsound anyway and should correspond as closely as possible to the old unsound encoding
2011-05-24, by blanchet
move lemmas to Extended_Reals and Extended_Real_Limits
2011-05-23, by hoelzl
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
2011-05-23, by krauss
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
2011-05-22, by krauss
fun command produces warning when patterns are incomplete (somewhat analogous to primrec)
2011-05-22, by krauss
added message when Waldmeister isn't run
2011-05-22, by blanchet
slightly improved documentation
2011-05-22, by blanchet
improved Waldmeister support -- even run it by default on unit equational goals
2011-05-22, by blanchet
fish out axioms in Waldmeister output
2011-05-22, by blanchet
removed SNARK hack now that SNARK is fixed
2011-05-22, by blanchet
recognize one more SystemOnTPTP error
2011-05-22, by blanchet
document Waldmeister
2011-05-22, by blanchet
added support for remote Waldmeister
2011-05-22, by blanchet
added Waldmeister
2011-05-22, by blanchet
reorganized ATP formats a little bit
2011-05-22, by blanchet
tuned;
2011-06-06, by wenzelm
removed odd remains of low-level session management;
2011-06-06, by wenzelm
moved incr_boundvars;
2011-06-06, by wenzelm
modernized and re-unified Thm.transfer;
2011-06-06, by wenzelm
removed obsolete material (superseded by implementation manual);
2011-06-06, by wenzelm
removed somewhat low-level stuff (cf. attribute "swapped" in isar-ref);
2011-06-05, by wenzelm
updated and re-unified classical proof methods;
2011-06-05, by wenzelm
tuned;
2011-06-05, by wenzelm
updated and re-unified classical rule declarations;
2011-06-05, by wenzelm
moved/updated introduction to Classical Reasoner;
2011-06-04, by wenzelm
tuned secref (still dangling);
2011-06-04, by wenzelm
updated and re-unified material on simprocs;
2011-06-03, by wenzelm
removed some old stuff;
2011-06-03, by wenzelm
tuned headings;
2011-06-02, by wenzelm
some material on "Generalized elimination and cases";
2011-06-02, by wenzelm
some material on "Structured induction proofs";
2011-06-02, by wenzelm
some material on "Structured Natural Deduction";
2011-06-01, by wenzelm
some material on "Calculational reasoning";
2011-06-01, by wenzelm
tuned;
2011-06-01, by wenzelm
added Synopsis, with some "Notepad" material;
2011-05-31, by wenzelm
more accurate deps;
2011-05-31, by wenzelm
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
2011-05-31, by wenzelm
moved/updated basic HOL overview;
2011-05-26, by wenzelm
updated and re-unified (co)inductive definitions in HOL;
2011-05-26, by wenzelm
clarified current 'primrec' vs. old 'recdef';
2011-05-26, by wenzelm
record examples;
2011-05-26, by wenzelm
updated and simplified HOL datatype examples (NB: special treatment of distinctness has been discontinued in the vicinity of 542b34b178ec);
2011-05-26, by wenzelm
updated and re-unified HOL rep_datatype;
2011-05-26, by wenzelm
rearranged some sections;
2011-05-25, by wenzelm
updated and re-unified HOL typedef, with some live examples;
2011-05-25, by wenzelm
optional jedit_build/etc/user-settings enable to override defaults produced by late component initialization;
2011-05-21, by wenzelm
merged
2011-05-21, by wenzelm
add divide_.._cancel, inverse_.._iff
2011-05-20, by hoelzl
add surj_vimage_empty
2011-05-20, by hoelzl
Add restricted borel measure to {0 .. 1}
2011-05-20, by hoelzl
equations for subsets of atLeastAtMost
2011-05-20, by hoelzl
build and run Isabelle/jEdit on the spot -- requires auxiliary "jedit_build" component;
2011-05-21, by wenzelm
misc tuning and update;
2011-05-21, by wenzelm
updated versions;
2011-05-20, by wenzelm
added Isabelle_Process.is_active;
2011-05-20, by wenzelm
update example
2011-05-20, by blanchet
name tuning
2011-05-20, by blanchet
further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
2011-05-20, by blanchet
prevent unsound combinator proofs in partially typed polymorphic type systems
2011-05-20, by blanchet
add lemma prob_finite_product
2011-05-20, by hoelzl
simp rules for empty intervals on dense linear order
2011-05-20, by hoelzl
merged
2011-05-20, by wenzelm
exercise more type systems (but only sound or quasi-sound ones)
2011-05-20, by blanchet
added see also
2011-05-20, by blanchet
document new type system and soundness properties of the different systems
2011-05-20, by blanchet
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
2011-05-20, by blanchet
reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts
2011-05-20, by blanchet
more doc fiddling
2011-05-20, by blanchet
more FAQs
2011-05-20, by blanchet
make sure the Vampire incomplete proof detection code kicks in
2011-05-20, by blanchet
automatically use "metisFT" when typed helpers are necessary
2011-05-20, by blanchet
tuning
2011-05-20, by blanchet
generate useful information for type axioms
2011-05-20, by blanchet
slightly fewer type predicates introduced in the lightweight encoding, based on the observation that only universal positive equalities are dangerous
2011-05-20, by blanchet
updated FAQ
2011-05-20, by blanchet
more informative message when Sledgehammer finds an unsound proof
2011-05-20, by blanchet
tuned proofs
2011-05-20, by haftmann
NEWS
2011-05-20, by haftmann
point-free characterization of operations on finite sets
2011-05-20, by haftmann
merged
2011-05-20, by haftmann
names of fold_set locales resemble name of characteristic property more closely
2011-05-20, by haftmann
clarified vacuous nature of predicate "transfer_morphism" -- equivalent to previous definiton
2011-05-20, by krauss
use point-free characterization for locale fun_left_comm_idem
2011-05-20, by haftmann
tuned proof
2011-05-20, by haftmann
Collect intro-rules for sigma-algebras
2011-05-17, by hoelzl
the measurable sets with null measure form a ring
2011-05-17, by hoelzl
add some lemmas for infinite product measure
2011-05-17, by hoelzl
add measurable_Least
2011-05-17, by hoelzl
add restrict_sigma
2011-05-17, by hoelzl
add borel_eq_atLeastLessThan
2011-05-17, by hoelzl
Add formalization of probabilistic independence for families of sets
2011-05-17, by hoelzl
add Bernoulli space
2011-05-19, by hoelzl
add product of probability spaces with finite cardinality
2011-05-19, by hoelzl
remove double sum_over_space_real_distribution
2011-05-19, by hoelzl
a deeper understanding of the code generation adaptation compared to 9079f49053e5
2011-05-19, by bulwahn
updated option documentation
2011-05-19, by blanchet
renamed "simple_types" to "simple"
2011-05-19, by blanchet
since we always default on the "_light" encoding (for good reasons, according to Judgment Day), get rid of that suffix
2011-05-19, by blanchet
tweaked ATP type systems further based on Judgment Day
2011-05-19, by blanchet
honor "conj_sym_kind" also for tag symbol declarations
2011-05-19, by blanchet
removed "poly_tags_light_bang" since highly unsound
2011-05-19, by blanchet
distinguish between a soft timeout (30 s by defalt) and a hard timeout (60 s), to let minimization-based provers (such as CVC3, Yices, and occasionally the other provers) do their job
2011-05-19, by blanchet
reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)
2011-05-19, by blanchet
fixed empty proof detection
2011-05-19, by blanchet
tuning
2011-05-19, by blanchet
minor doc fixes
2011-05-19, by blanchet
mention version 0.6 of Vampire, since that's what's currently available for download
2011-05-19, by blanchet
better error reporting: detect missing E proofs and remove Vampire native format error
2011-05-19, by blanchet
NEWS
2011-05-18, by bulwahn
adding Code_Char_ord to code generation regression tests
2011-05-18, by bulwahn
adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages
2011-05-18, by bulwahn
removed some obsolete text;
2011-05-20, by wenzelm
basic support for overpainting of text, imitating jEdit internals;
2011-05-18, by wenzelm
some support for token/chunk handling, imitating jEdit internals;
2011-05-17, by wenzelm
renamed thin to light, fat to heavy
2011-05-17, by blanchet
code cleanup, better handling of corner cases
2011-05-17, by blanchet
run blacklist algorithm only if slicing is on
2011-05-17, by blanchet
implemented thin versions of "preds" type systems + fixed various issues with type args
2011-05-17, by blanchet
use antiquotation
2011-05-17, by blanchet
renamed "shallow" to "thin" and make it the default
2011-05-17, by blanchet
more work on "shallow" encoding + adjustments to other encodings
2011-05-17, by blanchet
generate type classes predicates in new "shallow" encoding
2011-05-17, by blanchet
started implementing "shallow" type systems, based on ideas by Claessen et al.
2011-05-17, by blanchet
added syntax for "shallow" encodings
2011-05-17, by blanchet
provide isabellep as a method
2011-05-17, by blanchet
append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism
2011-05-17, by blanchet
tuned;
2011-05-16, by wenzelm
less fine-grained mira dependencies
2011-05-16, by krauss
mira hack for special settings on lxbroy10
2011-05-16, by krauss
no dependencies for Isabelle_makeall, which will be built in one go
2011-05-16, by krauss
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
2011-05-16, by krauss
future merge of grammars, to improve parallel performance;
2011-05-15, by wenzelm
only show relevant timing;
2011-05-15, by wenzelm
timing of Theory_Data operations, with implicit thread positions when functor is applied;
2011-05-15, by wenzelm
tuned;
2011-05-15, by wenzelm