blanchet [Wed, 03 Sep 2014 22:46:54 +0200] rev 58163
added tests for new 'countable_datatype' proof method
traytel [Wed, 03 Sep 2014 12:30:25 +0200] rev 58162
lessen the burden on the caller: sort where necessary in n2m
blanchet [Wed, 03 Sep 2014 09:43:00 +0200] rev 58161
added compatibility function
blanchet [Wed, 03 Sep 2014 00:31:38 +0200] rev 58160
added countable tactic for new-style datatypes
blanchet [Wed, 03 Sep 2014 00:31:37 +0200] rev 58159
tuning
blanchet [Wed, 03 Sep 2014 00:06:32 +0200] rev 58158
registered 'typerep' as countable again
blanchet [Wed, 03 Sep 2014 00:06:30 +0200] rev 58157
moved old datatype material around
blanchet [Wed, 03 Sep 2014 00:06:28 +0200] rev 58156
removed vacuous theorem references
blanchet [Wed, 03 Sep 2014 00:06:27 +0200] rev 58155
commented out failing tactic (now that 'typerep' is defined using the new package
blanchet [Wed, 03 Sep 2014 00:06:26 +0200] rev 58154
tuned imports