blanchet [Wed, 12 Feb 2014 08:35:57 +0100] rev 56756
renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 56755
adapted theories to '{case,rec}_{list,option}' names
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 56754
avoid old 'prod.simps' -- better be more specific
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 56753
repaired hard-coded constant names
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 56752
killed 'rep_compat' option
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 56751
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 56750
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 56749
use right local theory -- shows up when 'no_discs_sels' is set
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 56748
compatibility names
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 56747
use new selector support to define 'the', 'hd', 'tl'