giving up calling 'datatype_compat' in a locale -- causes trouble with extensions

ported 'Statespace' to support new datatypes as well

use 'datatype_new' in Quickcheck examples

more compatibility functions

codatatypes are not datatypes

ported Quickcheck to support new datatypes better

removed more slow Refute tests

tuned Refute example

Some work on the new waldmeister integration

merged

replay Z3 rewrite steps that lift if-then-else expressions

test discriminators/selectors in BNF regression suite

merge

made SML/NJ happier

tuning

silenced nonexhaustive primrec warnings

more convenient printing of real numbers after evaluation

avoid more 'bad background theory' issues

ported TFL to mixture of old and new datatypes

drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'

ported to use new-style datatypes * * * compile

ported Refute to use new datatypes when possible

renamed BNF theories

renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'

added primrec compatibility function

more work on compatibility interfaces

added compatibility examples/tests

implemented compatibility definition of datatype

implemented compatibility interpretation

compile

compile

tuning

compile

more compatibility between old- and new-style datatypes

added theory-based getters for convenience

made transfer functions slightly more general

tuned signatures

tuning

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

tuned structure inclusion

took out legacy material from 'HOL/Library/Library.thy'

removed commented out parts

tuned whitespace

document 'set_transfer'

generate 'set_transfer' for BNFs

document 'rel_transfer'

generate 'rel_transfer' for BNFs

document 'map_transfer'