2012-01-04 wenzelm 2012-01-04 updated version information; discontinued somewhat obsolete hotspot check: OpenJDK 1.7 works reasonably well, and final bundling provides certain tested JDK/JRE versions;
2012-01-04 nipkow 2012-01-04 generalised type
2012-01-04 blanchet 2012-01-04 improved "set" support by code inspection
2012-01-04 blanchet 2012-01-04 remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
2012-01-04 blanchet 2012-01-04 tuning
2012-01-04 blanchet 2012-01-04 handle higher-order occurrences of sets gracefully in model display
2012-01-04 wenzelm 2012-01-04 prefer explicit version information;
2012-01-04 blanchet 2012-01-04 more Nitpick doc updates
2012-01-04 blanchet 2012-01-04 reenable Kodkodi in Mira now that Nitpick has been ported to 'a set constructor
2012-01-04 blanchet 2012-01-04 reenable Kodkodi in Isatest now that Nitpick has been ported to 'a set constructor
2012-01-03 blanchet 2012-01-03 fixed bisimilarity axiom -- avoid "insert" with wrong type
2012-01-03 blanchet 2012-01-03 tuning
2012-01-03 blanchet 2012-01-03 updated Nitpick docs after "set" reintroduction
2012-01-03 blanchet 2012-01-03 no abuse of notation
2012-01-03 blanchet 2012-01-03 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 blanchet 2012-01-03 more robust destruction of "set Collect" idiom
2012-01-03 blanchet 2012-01-03 handle starred predicates correctly w.r.t. "set"
2012-01-03 blanchet 2012-01-03 handle "Id" gracefully w.r.t. "set"
2012-01-03 blanchet 2012-01-03 reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
2012-01-03 blanchet 2012-01-03 handle "set" correctly in Refute -- inspired by old code from Isabelle2007
2012-01-03 blanchet 2012-01-03 create consts with proper "set" types
2012-01-03 blanchet 2012-01-03 tuned Refute
2012-01-03 blanchet 2012-01-03 lower cardinality for faster testing
2012-01-03 blanchet 2012-01-03 simplify mem Collect
2012-01-03 blanchet 2012-01-03 tuning
2012-01-03 blanchet 2012-01-03 ported Minipick to "set"
2012-01-03 blanchet 2012-01-03 fixed set extensionality code
2012-01-03 blanchet 2012-01-03 tuned import
2012-01-03 blanchet 2012-01-03 construct correct "set" type for wf goal
2012-01-03 blanchet 2012-01-03 fixed Nitpick's typedef handling w.r.t. "set"
2012-01-03 blanchet 2012-01-03 fixed type annotations
2012-01-03 blanchet 2012-01-03 rationalized output (a bit)
2012-01-03 blanchet 2012-01-03 fixed a few more bugs in \Nitpick's new "set" support
2012-01-03 blanchet 2012-01-03 regenerate SMT example certificates, to reflect "set" type constructor
2012-01-03 blanchet 2012-01-03 port part of Nitpick to "set" type constructor
2012-01-03 blanchet 2012-01-03 reintroduced failing examples now that they work again, after reintroduction of "set"
2012-01-03 blanchet 2012-01-03 ported mono calculus to handle "set" type constructors
2012-01-03 blanchet 2012-01-03 fixed spurious catch-all patterns
2012-01-03 wenzelm 2012-01-03 more benchmarks; tuned;
2012-01-02 nipkow 2012-01-02 tuned
2012-01-02 blanchet 2012-01-02 ported "Sets" example to "set" type constructor
2012-01-02 blanchet 2012-01-02 ported a dozen of proofs to the "set" type constructor
2012-01-02 blanchet 2012-01-02 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 blanchet 2012-01-02 update docs to reflect "Manual_Nits"
2012-01-02 blanchet 2012-01-02 removed special handling for set constants in relevance filter
2012-01-02 blanchet 2012-01-02 reintroduced Sledgehammer call taken out by 9bc924006136, with some hints to guide the naive relevance filter
2012-01-02 blanchet 2012-01-02 killed unfold_set_const option that makes no sense now that set is a type constructor again
2012-01-02 nipkow 2012-01-02 tuned
2012-01-02 nipkow 2012-01-02 removed unnecessary lemmas
2012-01-02 nipkow 2012-01-02 tuned proofs
2012-01-01 nipkow 2012-01-01 tuned var names
2012-01-01 nipkow 2012-01-01 tuned argument order
2012-01-01 huffman 2012-01-01 merged
2011-12-30 huffman 2011-12-30 add simp rules for bitwise word operations with 1
2011-12-31 nipkow 2011-12-31 tuned types
2011-12-31 krauss 2011-12-31 disabled failing sledgehammer unit test (collateral damage of 184d36538e51)
2011-12-31 krauss 2011-12-31 disabled kodkodi in mira runs as well (cf. 493d9c4d7ed5)
2011-12-30 berghofe 2011-12-30 merged
2011-12-30 berghofe 2011-12-30 Made gen_dest_case more robust against eta contraction
2011-12-30 wenzelm 2011-12-30 merged