Sat, 07 Aug 2010 16:15:52 +0200 wenzelm more explicit treatment of Swing thread context;
Sat, 07 Aug 2010 14:45:26 +0200 wenzelm replaced individual Document_Model history by all-inclusive one in Session;
Sat, 07 Aug 2010 13:19:48 +0200 wenzelm misc tuning and clarification;
Fri, 06 Aug 2010 21:52:49 +0200 wenzelm avoid null in Scala;
Fri, 06 Aug 2010 14:37:04 +0200 wenzelm updated keywords;
Fri, 06 Aug 2010 14:35:04 +0200 wenzelm removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
Fri, 06 Aug 2010 12:38:02 +0200 wenzelm merged
Fri, 06 Aug 2010 11:37:33 +0200 blanchet merged
Fri, 06 Aug 2010 11:35:10 +0200 blanchet quotient types registered as codatatypes are no longer quotient types
Fri, 06 Aug 2010 11:33:58 +0200 blanchet added a friendly warning
Fri, 06 Aug 2010 11:05:57 +0200 blanchet extend the scope of limitation about nonconservative extensions
Fri, 06 Aug 2010 10:50:52 +0200 blanchet improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
Thu, 05 Aug 2010 22:29:43 +0200 ballarin Remove duplicate locale activation code; performance improvement.
Thu, 05 Aug 2010 21:56:22 +0200 blanchet added record field
Thu, 05 Aug 2010 20:17:50 +0200 blanchet added "whack"
Thu, 05 Aug 2010 18:33:07 +0200 blanchet handle "Rep_unit" & Co. gracefully
Thu, 05 Aug 2010 18:00:50 +0200 blanchet added support for "Abs_" and "Rep_" functions on quotient types
Thu, 05 Aug 2010 15:44:54 +0200 blanchet fiddle with specialization etc.
Thu, 05 Aug 2010 14:45:27 +0200 blanchet handle inductive predicates correctly after change in "def" semantics
Thu, 05 Aug 2010 14:32:24 +0200 blanchet don't specialize built-ins or constructors
Thu, 05 Aug 2010 14:20:34 +0200 blanchet more docs
Thu, 05 Aug 2010 14:10:18 +0200 blanchet prevent the expansion of too large definitions -- use equations for these instead
Thu, 05 Aug 2010 12:58:57 +0200 blanchet make nitpick accept "==" for "nitpick_(p)simp"s
Thu, 05 Aug 2010 12:40:12 +0200 blanchet fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
Thu, 05 Aug 2010 11:54:53 +0200 blanchet deal correctly with Pure.conjunction in mono check
Thu, 05 Aug 2010 09:49:46 +0200 blanchet rename internal functions
Thu, 05 Aug 2010 01:12:12 +0200 blanchet remove buggy and needless condition
Thu, 05 Aug 2010 00:21:11 +0200 blanchet renamed internal function
Wed, 04 Aug 2010 23:27:27 +0200 blanchet Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
Wed, 04 Aug 2010 22:47:52 +0200 blanchet avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
Wed, 04 Aug 2010 21:56:17 +0200 blanchet improve datatype symmetry breaking;
Wed, 04 Aug 2010 10:52:29 +0200 blanchet merged
Wed, 04 Aug 2010 10:51:04 +0200 blanchet make SML/NJ happy
Wed, 04 Aug 2010 10:39:35 +0200 blanchet get rid of all "optimizations" regarding "unit" and other cardinality-1 types
Tue, 03 Aug 2010 21:37:12 +0200 blanchet tuning
Tue, 03 Aug 2010 21:20:31 +0200 blanchet better "Pretty" handling
Tue, 03 Aug 2010 18:27:21 +0200 blanchet change formula for enumerating scopes
Tue, 03 Aug 2010 18:14:44 +0200 blanchet example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
Tue, 03 Aug 2010 17:43:15 +0200 blanchet speed up Nitpick examples a little bit
Tue, 03 Aug 2010 17:29:54 +0200 blanchet minor changes
Tue, 03 Aug 2010 17:29:27 +0200 blanchet updated example timings
Tue, 03 Aug 2010 15:15:17 +0200 blanchet more helpful message
Tue, 03 Aug 2010 14:54:30 +0200 blanchet also mention gfp
Tue, 03 Aug 2010 14:49:42 +0200 blanchet bump up the max cardinalities, to use up more of the time given to us by the user
Tue, 03 Aug 2010 14:49:02 +0200 blanchet make tracing monotonicity easier
Tue, 03 Aug 2010 14:28:44 +0200 blanchet more documentation, based on email discussions with a user
Tue, 03 Aug 2010 14:06:29 +0200 blanchet make example easier to parse
Tue, 03 Aug 2010 14:04:48 +0200 blanchet clarify attribute documentation
Tue, 03 Aug 2010 13:40:24 +0200 blanchet choose better example
Tue, 03 Aug 2010 13:29:26 +0200 blanchet fix newly introduced bug w.r.t. conditional equations
Tue, 03 Aug 2010 13:17:15 +0200 blanchet document something I explained in an email to a poweruser
Tue, 03 Aug 2010 12:31:30 +0200 blanchet make Nitpick more flexible when parsing (p)simp rules
Tue, 03 Aug 2010 12:16:32 +0200 blanchet fix soundness bug w.r.t. "Suc" with "binary_ints"
Tue, 03 Aug 2010 02:18:05 +0200 blanchet handle free variables even more gracefully;
Tue, 03 Aug 2010 01:16:08 +0200 blanchet optimize local "def"s by treating them as definitions
Mon, 02 Aug 2010 19:15:15 +0200 blanchet careful about which linear inductive predicates should be starred
Mon, 02 Aug 2010 18:52:51 +0200 blanchet help Nitpick
Mon, 02 Aug 2010 18:39:14 +0200 blanchet fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
Mon, 02 Aug 2010 16:29:36 +0200 blanchet prevent generation of needless specialized constants etc.
Mon, 02 Aug 2010 15:52:32 +0200 blanchet optimize generated Kodkod formula
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip