2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58278
documented extraction plugin
src/Doc/Datatypes/Datatypes.thy

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58277
made realizer more robust in the face of nesting through functions
src/HOL/Tools/datatype_realizer.ML

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58276
removed debugging junk
src/HOL/BNF_Least_Fixpoint.thy

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58275
renamed ML file and module
src/HOL/BNF_Least_Fixpoint.thy src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML src/HOL/Tools/datatype_realizer.ML

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58274
made datatype realizer plugin work for new-style datatypes with no nesting
src/HOL/BNF_Least_Fixpoint.thy src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML src/HOL/Tools/inductive_realizer.ML

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58273
ported HOL-Proofs-Lambda to new datatypes
src/HOL/Proofs/Lambda/Eta.thy src/HOL/Proofs/Lambda/Lambda.thy src/HOL/Proofs/Lambda/LambdaType.thy

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58272
ported HOL-Proofs-Extraction to new datatypes
src/HOL/Proofs/Extraction/Higman.thy src/HOL/Proofs/Extraction/Warshall.thy

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58271
made SML/NJ happier
src/HOL/Tools/BNF/bnf_lfp_compat.ML

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58270
more porting to new datatypes
src/HOL/HOLCF/IOA/NTP/Correctness.thy src/HOL/HOLCF/IOA/NTP/Impl.thy src/HOL/HOLCF/IOA/Storage/Correctness.thy src/HOL/Induct/Common_Patterns.thy

2014-09-09 blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58269
tuned IArray code generator w.r.t. map rel set
src/HOL/Library/IArray.thy