2010-12-07 bulwahn 2010-12-07 adding a definition for refl_on which is friendly for quickcheck and nitpick
2010-12-07 blanchet 2010-12-07 merged
2010-12-07 blanchet 2010-12-07 simplify monotonicity code after killing "fin_fun" optimization
2010-12-07 blanchet 2010-12-07 updated Nitpick's documentation w.r.t. finitization
2010-12-07 blanchet 2010-12-07 remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
2010-12-07 blanchet 2010-12-07 give the inner timeout mechanism a chance, since it gives more precise information to the user
2010-12-07 blanchet 2010-12-07 updated monotonicity calculus w.r.t. set products
2010-12-07 blanchet 2010-12-07 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 blanchet 2010-12-07 added a hint when the user obviously just forgot a colon after the lemma's name
2010-12-07 blanchet 2010-12-07 simplified special handling of set products
2010-12-07 blanchet 2010-12-07 fix special handling of set products
2010-12-07 blanchet 2010-12-07 use heuristic to determine whether to keep or drop an existing "let" -- and drop all higher-order lets
2010-12-07 bulwahn 2010-12-07 merged
2010-12-07 bulwahn 2010-12-07 testing smartly in two dimensions (cardinality and size) in quickcheck
2010-12-07 blanchet 2010-12-07 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
2010-12-07 blanchet 2010-12-07 make SML/NJ happy
2010-12-07 blanchet 2010-12-07 merge
2010-12-06 blanchet 2010-12-06 show strings as "s_1" etc. rather than "l_1" etc.
2010-12-06 blanchet 2010-12-06 quiet Metis in "try"
2010-12-07 haftmann 2010-12-07 removed experimental equality checking of closures; acknowledge underapproximation of equality in function name
2010-12-06 huffman 2010-12-06 add set-union-like syntax for powerdomain bind operators
2010-12-06 huffman 2010-12-06 merged
2010-12-06 huffman 2010-12-06 instance unit :: domain
2010-12-06 huffman 2010-12-06 simplify ideal completion proofs
2010-12-06 huffman 2010-12-06 remove unused lemmas
2010-12-06 huffman 2010-12-06 remove lemma cont_cfun; rename thelub_cfun to lub_cfun
2010-12-06 huffman 2010-12-06 rename lub_fun -> is_lub_fun, thelub_fun -> lub_fun
2010-12-06 huffman 2010-12-06 pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
2010-12-06 huffman 2010-12-06 cpodef no longer generates lemma is_lub_foo, since it is redundant with lub_foo
2010-12-06 huffman 2010-12-06 add lemmas lub_APP, lub_LAM
2010-12-06 hoelzl 2010-12-06 folding on arbitrary Lebesgue integrable functions
2010-12-06 hoelzl 2010-12-06 fixed spelling errors
2010-12-06 hoelzl 2010-12-06 move coercions to appropriate places
2010-12-03 hoelzl 2010-12-03 it is known as the extended reals, not the infinite reals
2010-12-06 nipkow 2010-12-06 moved coercion decl. for int
2010-12-06 bulwahn 2010-12-06 adapting copied bash code in mutabelle script
2010-12-06 wenzelm 2010-12-06 more correct NEWS;
2010-12-06 wenzelm 2010-12-06 merged
2010-12-06 blanchet 2010-12-06 fix monotonicity type of None
2010-12-06 blanchet 2010-12-06 compile
2010-12-06 blanchet 2010-12-06 introduced hack to exploit the symmetry of equality in monotonicity calculus
2010-12-06 blanchet 2010-12-06 cleanup example
2010-12-06 blanchet 2010-12-06 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 blanchet 2010-12-06 fixed bug in monotonicity solution display, whereby the polarity of literals was ignored
2010-12-06 blanchet 2010-12-06 improve precision of forall in constancy part of the monotonicity calculus
2010-12-06 blanchet 2010-12-06 added some missing well-annotatedness constraints to monotonicity calculus
2010-12-06 blanchet 2010-12-06 more work on the monotonicity evaluation driver
2010-12-06 blanchet 2010-12-06 improve precision of finite functions in monotonicity calculus
2010-12-06 blanchet 2010-12-06 added ML code for testing entire theories for monotonicity
2010-12-06 blanchet 2010-12-06 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 blanchet 2010-12-06 added examples to exercise new monotonicity code
2010-12-06 blanchet 2010-12-06 fixed quantifier handling of new monotonicity calculus
2010-12-06 blanchet 2010-12-06 tune parentheses and indentation
2010-12-06 blanchet 2010-12-06 proper handling of frames for connectives in monotonicity calculus
2010-12-06 blanchet 2010-12-06 tune indentation
2010-12-06 blanchet 2010-12-06 removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
2010-12-06 blanchet 2010-12-06 implemented All rules from new monotonicity calculus
2010-12-06 blanchet 2010-12-06 fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints
2010-12-06 blanchet 2010-12-06 started implementing the new monotonicity rules for application
2010-12-06 blanchet 2010-12-06 implemented connectives in new monotonicity calculus