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

implemented Auto Sledgehammer
2010-09-11, by blanchet
document changes to Auto Nitpick
2010-09-11, by blanchet
change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
2010-09-11, by blanchet
always handle type variables in typedefs as global
2010-09-11, by blanchet
removed duplicate lemma
2010-09-14, by nipkow
adding two more examples to example theory
2010-09-13, by bulwahn
handling function types more carefully than in e98a06145530
2010-09-13, by bulwahn
adding order on modes
2010-09-13, by bulwahn
removing obsolete argument in prepare_intrs; passing context instead of theory in prepare_intrs
2010-09-13, by bulwahn
type antiquotation: allow arbitrary type abbreviations, but fail with user-space exception on bad input
2010-09-13, by haftmann
merged
2010-09-13, by haftmann
added Imperative HOL overview
2010-09-13, by haftmann
print mode for Imperative HOL overview; tuned and more accurate dependencies
2010-09-13, by haftmann
'class' and 'type' are now antiquoations by default
2010-09-13, by haftmann
merged
2010-09-13, by wenzelm
merged
2010-09-13, by nipkow
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-13, by nipkow
added and renamed lemmas
2010-09-13, by nipkow
merged
2010-09-13, by bulwahn
directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory
2010-09-10, by bulwahn
added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet
2010-09-13, by boehmes
use eta-contracted version for occurrence check (avoids possible non-termination)
2010-09-10, by krauss
tuned signature;
2010-09-13, by wenzelm
Type_Infer.finish: index 0 -- freshness supposedly via Name.invents;
2010-09-13, by wenzelm
simplified Type_Infer: eliminated separate datatypes pretyp/preterm -- only assign is_paramT TVars;
2010-09-13, by wenzelm
tuned;
2010-09-13, by wenzelm
Type_Infer.preterm: eliminated separate Constraint;
2010-09-12, by wenzelm
Type_Infer.infer_types: plain error instead of kernel exception TYPE;
2010-09-12, by wenzelm
load type_infer.ML later -- proper context for Type_Infer.infer_types;
2010-09-12, by wenzelm
common Type.appl_error, which also covers explicit constraints;
2010-09-12, by wenzelm
eliminated aliases of Type.constraint;
2010-09-12, by wenzelm
tuned;
2010-09-12, by wenzelm
tuned messages;
2010-09-12, by wenzelm
avoid extra wrapping for interrupts;
2010-09-10, by wenzelm
tuned markup;
2010-09-09, by wenzelm
updated keywords;
2010-09-10, by wenzelm
proper antiquotations;
2010-09-10, by wenzelm
fixed antiquotation;
2010-09-10, by wenzelm
updated generated file;
2010-09-10, by wenzelm
updated config options;
2010-09-10, by wenzelm
removed spurious addition from 9e58f0499f57;
2010-09-10, by wenzelm
merged
2010-09-10, by wenzelm
improved error message for common mistake (fun f where "g x = ...")
2010-09-10, by krauss
adding another String.literal example
2010-09-10, by bulwahn
fiddling with the correct setup for String.literal
2010-09-10, by bulwahn
refactoring mode inference so that the theory is not changed in the mode inference procedure
2010-09-10, by bulwahn
Haskell == is infix, not infixl
2010-09-10, by haftmann
more correct dependencies
2010-09-10, by haftmann
merged
2010-09-09, by blanchet
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
2010-09-09, by blanchet
use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way
2010-09-09, by blanchet
clarify comment
2010-09-09, by blanchet
improve on 65903ec4e8e8: fix more "add_ffpair" exceptions in failed ATP proofs
2010-09-09, by blanchet
allow Sledgehammer proofs containing nameless local facts with schematic variables in them
2010-09-09, by blanchet
tuning
2010-09-09, by blanchet
more precise error messages when Vampire is interrupted or SPASS runs into an internal bug
2010-09-09, by blanchet
better error reporting when the Sledgehammer minimizer is interrupted
2010-09-09, by blanchet
add cutoff beyond which facts are handled using definitional CNF
2010-09-09, by blanchet
"resurrected" a Metis proof
2010-09-09, by blanchet
replace two slow "metis" proofs with faster proofs
2010-09-09, by blanchet

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

isabelle