isabelle: Graph

tuned
2010-12-08, by haftmann
nice syntax for lattice INFI, SUPR;
2010-12-08, by haftmann
NEWS
2010-12-08, by haftmann
adding more efficient implementations for quantifiers in Enum
2010-12-08, by bulwahn
improving the mutabelle script
2010-12-08, by bulwahn
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`;
2010-12-08, by haftmann
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
2010-12-08, by haftmann
hide popular names R and B
2010-12-08, by haftmann
built-in numbers are also built-in terms
2010-12-08, by boehmes
be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
2010-12-08, by boehmes
merged
2010-12-07, by haftmann
more concise case names; proved extensionality
2010-12-07, by haftmann
name filter operation just filter (c.f. List.filter and list comprehension syntax)
2010-12-07, by haftmann
tuned whitespace
2010-12-07, by haftmann
eliminated some hard tabulators (deprecated);
2010-12-07, by wenzelm
pass constant arguments to the built-in check function, cf. d2b1fc1b8e19
2010-12-07, by blanchet
merged
2010-12-07, by boehmes
updated SMT certificates
2010-12-07, by boehmes
reduced unnecessary complexity; improved documentation; tuned
2010-12-07, by boehmes
tuned
2010-12-07, by boehmes
centralized handling of built-in types and constants for bitvectors
2010-12-07, by boehmes
moved smt_word.ML into the directory of the Word library
2010-12-07, by boehmes
centralized handling of built-in types and constants;
2010-12-07, by boehmes
more aggressive unfolding of unknowns in Z3 models
2010-12-06, by boehmes
tuned
2010-12-06, by boehmes
adding a definition for refl_on which is friendly for quickcheck and nitpick
2010-12-07, by bulwahn
merged
2010-12-07, by blanchet
simplify monotonicity code after killing "fin_fun" optimization
2010-12-07, by blanchet
updated Nitpick's documentation w.r.t. finitization
2010-12-07, by blanchet
remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
2010-12-07, by blanchet
give the inner timeout mechanism a chance, since it gives more precise information to the user
2010-12-07, by blanchet
updated monotonicity calculus w.r.t. set products
2010-12-07, by blanchet
removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
2010-12-07, by blanchet
added a hint when the user obviously just forgot a colon after the lemma's name
2010-12-07, by blanchet
simplified special handling of set products
2010-12-07, by blanchet
fix special handling of set products
2010-12-07, by blanchet
use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
2010-12-07, by blanchet
merged
2010-12-07, by bulwahn
testing smartly in two dimensions (cardinality and size) in quickcheck
2010-12-07, by bulwahn
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
2010-12-07, by blanchet
make SML/NJ happy
2010-12-07, by blanchet
merge
2010-12-07, by blanchet
show strings as "s_1" etc. rather than "l_1" etc.
2010-12-06, by blanchet
quiet Metis in "try"
2010-12-06, by blanchet
removed experimental equality checking of closures; acknowledge underapproximation of equality in function name
2010-12-07, by haftmann
add set-union-like syntax for powerdomain bind operators
2010-12-06, by huffman
merged
2010-12-06, by huffman
instance unit :: domain
2010-12-06, by huffman
simplify ideal completion proofs
2010-12-06, by huffman
remove unused lemmas
2010-12-06, by huffman
remove lemma cont_cfun;
2010-12-06, by huffman
rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
2010-12-06, by huffman
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
2010-12-06, by huffman
cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo
2010-12-06, by huffman
add lemmas lub_APP, lub_LAM
2010-12-06, by huffman
folding on arbitrary Lebesgue integrable functions
2010-12-06, by hoelzl
fixed spelling errors
2010-12-06, by hoelzl
move coercions to appropriate places
2010-12-06, by hoelzl
it is known as the extended reals, not the infinite reals
2010-12-03, by hoelzl
moved coercion decl. for int
2010-12-06, by nipkow
adapting copied bash code in mutabelle script
2010-12-06, by bulwahn
more correct NEWS;
2010-12-06, by wenzelm
merged
2010-12-06, by wenzelm
fix monotonicity type of None
2010-12-06, by blanchet
compile
2010-12-06, by blanchet
introduced hack to exploit the symmetry of equality in monotonicity calculus
2010-12-06, by blanchet
cleanup example
2010-12-06, by blanchet
add more flexibility to the monotonicity calculus: instead of hardcoding F-arrows, also allow G-arrows, simulating applications of the Sub rule
2010-12-06, by blanchet
fixed bug in monotonicity solution display, whereby the polarity of literals was ignored
2010-12-06, by blanchet
improve precision of forall in constancy part of the monotonicity calculus
2010-12-06, by blanchet
added some missing well-annotatedness constraints to monotonicity calculus
2010-12-06, by blanchet
more work on the monotonicity evaluation driver
2010-12-06, by blanchet
improve precision of finite functions in monotonicity calculus
2010-12-06, by blanchet
added ML code for testing entire theories for monotonicity
2010-12-06, by blanchet
use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus
2010-12-06, by blanchet
added examples to exercise new monotonicity code
2010-12-06, by blanchet
fixed quantifier handling of new monotonicity calculus
2010-12-06, by blanchet
tune parentheses and indentation
2010-12-06, by blanchet
proper handling of frames for connectives in monotonicity calculus
2010-12-06, by blanchet
tune indentation
2010-12-06, by blanchet
removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
2010-12-06, by blanchet
implemented All rules from new monotonicity calculus
2010-12-06, by blanchet
fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints
2010-12-06, by blanchet
started implementing the new monotonicity rules for application
2010-12-06, by blanchet
implemented connectives in new monotonicity calculus
2010-12-06, by blanchet
added "Neq" operator to monotonicity inference module
2010-12-06, by blanchet
started implementing connectives in new monotonicity calculus
2010-12-06, by blanchet
more work on frames in the new monotonicity calculus
2010-12-06, by blanchet
support 3 monotonicity calculi in one and fix soundness bug
2010-12-06, by blanchet
tuning
2010-12-06, by blanchet
proper handling of assignment disjunctions vs. conjunctions
2010-12-06, by blanchet
adapt monotonicity code to four annotation types
2010-12-06, by blanchet
more monotonicity tuning
2010-12-06, by blanchet
tuning
2010-12-06, by blanchet
added frame component to Gamma in monotonicity calculus
2010-12-06, by blanchet
use boolean pair to encode annotation, which may now take four values
2010-12-06, by blanchet
started generalizing monotonicity code to accommodate new calculus
2010-12-06, by blanchet
merged
2010-12-06, by blanchet
handle "max_relevant" uniformly
2010-12-06, by blanchet
honor the default max relevant facts setting from the SMT solvers in Sledgehammer
2010-12-06, by blanchet
have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts?
2010-12-06, by blanchet
return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
2010-12-06, by blanchet
trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
2010-12-06, by blanchet
reraise interrupt exceptions
2010-12-06, by blanchet
[mq]: sledge_binary_minimizer
2010-12-06, by blanchet
correcting usage documentation in mirabelle tool
2010-12-06, by bulwahn
adding mutabelle as a component and an isabelle tool to be used in regression testing
2010-12-06, by bulwahn
commenting out sledgehammer_mtd in Mutabelle
2010-12-06, by bulwahn
removing declaration in quickcheck to really enable exhaustive testing
2010-12-06, by bulwahn
adding timeout to try invocation in mutabelle
2010-12-06, by bulwahn
adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
2010-12-06, by bulwahn
replace `type_mapper` by the more adequate `type_lifting`
2010-12-06, by haftmann
moved bootstrap of type_lifting to Fun
2010-12-06, by haftmann
replace `type_mapper` by the more adequate `type_lifting`
2010-12-06, by haftmann
avoid explicit encoding -- acknowledge UTF-8 as global default and Isabelle/jEdit preference of UTF-8-Isabelle;
2010-12-06, by wenzelm
IsabelleText font: include Cyrillic, Hebrew, Arabic from DejaVu Sans 2.32;
2010-12-05, by wenzelm
command 'notepad' replaces former 'example_proof';
2010-12-05, by wenzelm
prefer 'notepad' over 'example_proof';
2010-12-05, by wenzelm
merged
2010-12-05, by haftmann
more intimate definition of fold_list / fold_once in terms of fold
2010-12-04, by haftmann