2012-01-03 ago blanchet always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
2012-01-03 ago blanchet more robust destruction of "set Collect" idiom
2012-01-03 ago blanchet handle starred predicates correctly w.r.t. "set"
2012-01-03 ago blanchet handle "Id" gracefully w.r.t. "set"
2012-01-03 ago blanchet reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
2012-01-03 ago blanchet handle "set" correctly in Refute -- inspired by old code from Isabelle2007
2012-01-03 ago blanchet create consts with proper "set" types
2012-01-03 ago blanchet tuned Refute
2012-01-03 ago blanchet lower cardinality for faster testing
2012-01-03 ago blanchet simplify mem Collect
2012-01-03 ago blanchet tuning
2012-01-03 ago blanchet ported Minipick to "set"
2012-01-03 ago blanchet fixed set extensionality code
2012-01-03 ago blanchet tuned import
2012-01-03 ago blanchet construct correct "set" type for wf goal
2012-01-03 ago blanchet fixed Nitpick's typedef handling w.r.t. "set"
2012-01-03 ago blanchet fixed type annotations
2012-01-03 ago blanchet rationalized output (a bit)
2012-01-03 ago blanchet fixed a few more bugs in \Nitpick's new "set" support
2012-01-03 ago blanchet regenerate SMT example certificates, to reflect "set" type constructor
2012-01-03 ago blanchet port part of Nitpick to "set" type constructor
2012-01-03 ago blanchet reintroduced failing examples now that they work again, after reintroduction of "set"
2012-01-03 ago blanchet ported mono calculus to handle "set" type constructors
2012-01-03 ago blanchet fixed spurious catch-all patterns
2012-01-03 ago wenzelm more benchmarks;
2012-01-02 ago nipkow tuned
2012-01-02 ago blanchet ported "Sets" example to "set" type constructor
2012-01-02 ago blanchet ported a dozen of proofs to the "set" type constructor
2012-01-02 ago blanchet reintroduced "metis" call taken out after reintroducing "set" as a constructor, and added two "metis" calls that used to be too slow
2012-01-02 ago blanchet update docs to reflect "Manual_Nits"
2012-01-02 ago blanchet removed special handling for set constants in relevance filter
2012-01-02 ago blanchet reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter
2012-01-02 ago blanchet killed unfold_set_const option that makes no sense now that set is a type constructor again
2012-01-02 ago nipkow tuned
2012-01-02 ago nipkow removed unnecessary lemmas
2012-01-02 ago nipkow tuned proofs
2012-01-01 ago nipkow tuned var names
2012-01-01 ago nipkow tuned argument order
2012-01-01 ago huffman merged
2011-12-30 ago huffman add simp rules for bitwise word operations with 1
2011-12-31 ago nipkow tuned types
2011-12-31 ago krauss disabled failing sledgehammer unit test (collateral damage of 184d36538e51)
2011-12-31 ago krauss disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5)
2011-12-30 ago berghofe merged
2011-12-30 ago berghofe Made gen_dest_case more robust against eta contraction
2011-12-30 ago wenzelm merged
2011-12-30 ago huffman remove unnecessary intermediate lemmas
2011-12-30 ago wenzelm tuned;
2011-12-30 ago wenzelm eliminated old-fashioned Global_Theory.add_thms;
2011-12-30 ago wenzelm simplified proof -- avoid res_inst_tac, afford plain asm_full_simp_tac;
2011-12-30 ago wenzelm simplified proof;
2011-12-30 ago wenzelm simplified proof;
2011-12-30 ago wenzelm simplified proof;
2011-12-30 ago wenzelm more parallelism;
2011-12-30 ago wenzelm tuned;
2011-12-29 ago wenzelm merged
2011-12-29 ago wenzelm tuned -- afford slightly larger simpset in simp_defs_tac;
2011-12-29 ago wenzelm tuned -- standard proofs by default;
2011-12-29 ago wenzelm do not fork skipped proofs;
2011-12-29 ago wenzelm clarified timeit_msg;