huffman [Thu, 12 Sep 2013 09:33:36 -0700] rev 53596
new lemmas
huffman [Thu, 12 Sep 2013 09:06:46 -0700] rev 53595
prefer theorem name over 'long_thm_list(n)'
huffman [Thu, 12 Sep 2013 09:04:46 -0700] rev 53594
prefer attribute 'unfolded thm' to 'simplified'
huffman [Thu, 12 Sep 2013 09:03:52 -0700] rev 53593
removed outdated comments
blanchet [Fri, 13 Sep 2013 02:55:04 +0200] rev 53592
made non-co case more robust as well (cf. b6e2993fd0d3)
blanchet [Fri, 13 Sep 2013 02:26:59 +0200] rev 53591
don't wrongly destroy sum types in coiterators
blanchet [Fri, 13 Sep 2013 00:55:44 +0200] rev 53590
beware of multi-constructor datatypes (cf. 27c418b7b985)
blanchet [Fri, 13 Sep 2013 00:39:24 +0200] rev 53589
beware of single-constructor datatypes, with no discriminators
traytel [Thu, 12 Sep 2013 23:43:02 +0200] rev 53588
more robust tactic to cover another corner case (added as example);
blanchet [Thu, 12 Sep 2013 23:29:13 +0200] rev 53587
generalized data structure, for extension with SMT solver proofs