2010-08-06 wenzelm 2010-08-06 updated keywords;
2010-08-06 wenzelm 2010-08-06 removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
2010-08-06 wenzelm 2010-08-06 merged
2010-08-06 blanchet 2010-08-06 merged
2010-08-06 blanchet 2010-08-06 quotient types registered as codatatypes are no longer quotient types
2010-08-06 blanchet 2010-08-06 added a friendly warning
2010-08-06 blanchet 2010-08-06 extend the scope of limitation about nonconservative extensions
2010-08-06 blanchet 2010-08-06 improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-05 ballarin 2010-08-05 Remove duplicate locale activation code; performance improvement.
2010-08-05 blanchet 2010-08-05 added record field
2010-08-05 blanchet 2010-08-05 added "whack"
2010-08-05 blanchet 2010-08-05 handle "Rep_unit" & Co. gracefully
2010-08-05 blanchet 2010-08-05 added support for "Abs_" and "Rep_" functions on quotient types
2010-08-05 blanchet 2010-08-05 fiddle with specialization etc.
2010-08-05 blanchet 2010-08-05 handle inductive predicates correctly after change in "def" semantics
2010-08-05 blanchet 2010-08-05 don't specialize built-ins or constructors
2010-08-05 blanchet 2010-08-05 more docs
2010-08-05 blanchet 2010-08-05 prevent the expansion of too large definitions -- use equations for these instead
2010-08-05 blanchet 2010-08-05 make nitpick accept "==" for "nitpick_(p)simp"s
2010-08-05 blanchet 2010-08-05 fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
2010-08-05 blanchet 2010-08-05 deal correctly with Pure.conjunction in mono check
2010-08-05 blanchet 2010-08-05 rename internal functions
2010-08-05 blanchet 2010-08-05 remove buggy and needless condition
2010-08-05 blanchet 2010-08-05 renamed internal function
2010-08-04 blanchet 2010-08-04 Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities
2010-08-04 blanchet 2010-08-04 avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
2010-08-04 blanchet 2010-08-04 improve datatype symmetry breaking; all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example
2010-08-04 blanchet 2010-08-04 merged
2010-08-04 blanchet 2010-08-04 make SML/NJ happy
2010-08-04 blanchet 2010-08-04 get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-03 blanchet 2010-08-03 tuning
2010-08-03 blanchet 2010-08-03 better "Pretty" handling
2010-08-03 blanchet 2010-08-03 change formula for enumerating scopes
2010-08-03 blanchet 2010-08-03 example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
2010-08-03 blanchet 2010-08-03 speed up Nitpick examples a little bit
2010-08-03 blanchet 2010-08-03 minor changes
2010-08-03 blanchet 2010-08-03 updated example timings
2010-08-03 blanchet 2010-08-03 more helpful message
2010-08-03 blanchet 2010-08-03 also mention gfp
2010-08-03 blanchet 2010-08-03 bump up the max cardinalities, to use up more of the time given to us by the user
2010-08-03 blanchet 2010-08-03 make tracing monotonicity easier
2010-08-03 blanchet 2010-08-03 more documentation, based on email discussions with a user
2010-08-03 blanchet 2010-08-03 make example easier to parse
2010-08-03 blanchet 2010-08-03 clarify attribute documentation
2010-08-03 blanchet 2010-08-03 choose better example
2010-08-03 blanchet 2010-08-03 fix newly introduced bug w.r.t. conditional equations
2010-08-03 blanchet 2010-08-03 document something I explained in an email to a poweruser
2010-08-03 blanchet 2010-08-03 make Nitpick more flexible when parsing (p)simp rules
2010-08-03 blanchet 2010-08-03 fix soundness bug w.r.t. "Suc" with "binary_ints"
2010-08-03 blanchet 2010-08-03 handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld
2010-08-03 blanchet 2010-08-03 optimize local "def"s by treating them as definitions
2010-08-02 blanchet 2010-08-02 careful about which linear inductive predicates should be starred
2010-08-02 blanchet 2010-08-02 help Nitpick
2010-08-02 blanchet 2010-08-02 fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
2010-08-02 blanchet 2010-08-02 prevent generation of needless specialized constants etc.
2010-08-02 blanchet 2010-08-02 optimize generated Kodkod formula
2010-08-02 blanchet 2010-08-02 prefer implication to equality, to be more SAT solver friendly
2010-08-02 blanchet 2010-08-02 minor symmetry breaking for codatatypes like llist
2010-08-02 blanchet 2010-08-02 fix bug with mutually recursive and nested codatatypes
2010-08-01 blanchet 2010-08-01 fix minor bug in sym breaking