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
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55405
use new selector support to define 'the', 'hd', 'tl'
blanchet [Wed, 12 Feb 2014 08:35:56 +0100] rev 55404
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well)
* * *
compile
* * *
tuned imports to prevent merge issues in 'Main'