Wed, 12 Feb 2014 08:35:56 +0100 killed 'rep_compat' option
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55410
killed 'rep_compat' option
Wed, 12 Feb 2014 08:35:56 +0100 made 'ctr_sugar' more friendly to the 'datatype_realizer'
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55409
made 'ctr_sugar' more friendly to the 'datatype_realizer' * * * reverted changes to 'datatype_realizer.ML'
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 tip