blanchet [Wed, 12 Feb 2014 08:35:57 +0100] rev 55415
renamed 'nat_{case,rec}' to '{case,rec}_nat'
blanchet [Wed, 12 Feb 2014 08:35:57 +0100] rev 55414
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55413
adapted theories to '{case,rec}_{list,option}' names
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55412
avoid old 'prod.simps' -- better be more specific
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55411
repaired hard-coded constant names
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55410
killed 'rep_compat' option
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'
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55408
use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55407
use right local theory -- shows up when 'no_discs_sels' is set
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55406
compatibility names