blanchet [Fri, 06 Aug 2010 11:35:10 +0200] rev 38215
quotient types registered as codatatypes are no longer quotient types
blanchet [Fri, 06 Aug 2010 11:33:58 +0200] rev 38214
added a friendly warning
blanchet [Fri, 06 Aug 2010 11:05:57 +0200] rev 38213
extend the scope of limitation about nonconservative extensions
blanchet [Fri, 06 Aug 2010 10:50:52 +0200] rev 38212
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
ballarin [Thu, 05 Aug 2010 22:29:43 +0200] rev 38211
Remove duplicate locale activation code; performance improvement.
blanchet [Thu, 05 Aug 2010 21:56:22 +0200] rev 38210
added record field
blanchet [Thu, 05 Aug 2010 20:17:50 +0200] rev 38209
added "whack"
blanchet [Thu, 05 Aug 2010 18:33:07 +0200] rev 38208
handle "Rep_unit" & Co. gracefully
blanchet [Thu, 05 Aug 2010 18:00:50 +0200] rev 38207
added support for "Abs_" and "Rep_" functions on quotient types
blanchet [Thu, 05 Aug 2010 15:44:54 +0200] rev 38206
fiddle with specialization etc.
blanchet [Thu, 05 Aug 2010 14:45:27 +0200] rev 38205
handle inductive predicates correctly after change in "def" semantics
blanchet [Thu, 05 Aug 2010 14:32:24 +0200] rev 38204
don't specialize built-ins or constructors
blanchet [Thu, 05 Aug 2010 14:20:34 +0200] rev 38203
more docs
blanchet [Thu, 05 Aug 2010 14:10:18 +0200] rev 38202
prevent the expansion of too large definitions -- use equations for these instead
blanchet [Thu, 05 Aug 2010 12:58:57 +0200] rev 38201
make nitpick accept "==" for "nitpick_(p)simp"s
blanchet [Thu, 05 Aug 2010 12:40:12 +0200] rev 38200
fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
blanchet [Thu, 05 Aug 2010 11:54:53 +0200] rev 38199
deal correctly with Pure.conjunction in mono check
blanchet [Thu, 05 Aug 2010 09:49:46 +0200] rev 38198
rename internal functions
blanchet [Thu, 05 Aug 2010 01:12:12 +0200] rev 38197
remove buggy and needless condition
blanchet [Thu, 05 Aug 2010 00:21:11 +0200] rev 38196
renamed internal function
blanchet [Wed, 04 Aug 2010 23:27:27 +0200] rev 38195
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
blanchet [Wed, 04 Aug 2010 22:47:52 +0200] rev 38194
avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
blanchet [Wed, 04 Aug 2010 21:56:17 +0200] rev 38193
improve datatype symmetry breaking;
all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example
blanchet [Wed, 04 Aug 2010 10:52:29 +0200] rev 38192
merged
blanchet [Wed, 04 Aug 2010 10:51:04 +0200] rev 38191
make SML/NJ happy
blanchet [Wed, 04 Aug 2010 10:39:35 +0200] rev 38190
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
blanchet [Tue, 03 Aug 2010 21:37:12 +0200] rev 38189
tuning
blanchet [Tue, 03 Aug 2010 21:20:31 +0200] rev 38188
better "Pretty" handling
blanchet [Tue, 03 Aug 2010 18:27:21 +0200] rev 38187
change formula for enumerating scopes
blanchet [Tue, 03 Aug 2010 18:14:44 +0200] rev 38186
example tweaking -- also prevents Nitpick_Tests from using more than 1 thread