2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:26 +0200] rev 58154
tuned imports
src/HOL/Main.thy src/HOL/Num.thy src/HOL/Option.thy

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:25 +0200] rev 58153
use 'datatype_new'
src/HOL/Extraction.thy

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:24 +0200] rev 58152
use 'datatype_new' in 'Main'
src/HOL/Code_Evaluation.thy src/HOL/Enum.thy src/HOL/Groups_List.thy src/HOL/Lazy_Sequence.thy src/HOL/Main.thy src/HOL/Nitpick.thy src/HOL/Num.thy src/HOL/Predicate.thy src/HOL/Quickcheck_Exhaustive.thy src/HOL/Quickcheck_Narrowing.thy src/HOL/Quickcheck_Random.thy src/HOL/Record.thy src/HOL/String.thy src/HOL/Typerep.thy

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:23 +0200] rev 58151
take out 'x = C' of the simplifier for unit types
src/Doc/Datatypes/Datatypes.thy src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:22 +0200] rev 58150
giving up calling 'datatype_compat' in a locale -- causes trouble with extensions
src/HOL/BNF_Examples/Compat.thy

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:22 +0200] rev 58149
ported 'Statespace' to support new datatypes as well
src/HOL/Statespace/state_fun.ML

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:21 +0200] rev 58148
use 'datatype_new' in Quickcheck examples
src/HOL/Quickcheck_Examples/Hotel_Example.thy src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy src/HOL/Quickcheck_Examples/Quickcheck_Interfaces.thy src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:19 +0200] rev 58147
more compatibility functions
src/HOL/BNF_Least_Fixpoint.thy src/HOL/Tools/BNF/bnf_lfp_compat.ML

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:18 +0200] rev 58146
codatatypes are not datatypes
src/HOL/Complex.thy src/HOL/Tools/BNF/bnf_lfp_compat.ML

2014-09-03 blanchet [Wed, 03 Sep 2014 00:06:17 +0200] rev 58145
ported Quickcheck to support new datatypes better
src/HOL/Tools/Quickcheck/exhaustive_generators.ML src/HOL/Tools/Quickcheck/quickcheck_common.ML