isabelle: Changelog

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58282

hide DEADID/ID theorems

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58281

tuning

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58280

more canonical (and correct) local theory threading

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58279

removed 'datatype_compat's that are no longer needed

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58278

documented extraction plugin

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58277

made realizer more robust in the face of nesting through functions

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58276

removed debugging junk

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58275

renamed ML file and module

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58274

made datatype realizer plugin work for new-style datatypes with no nesting

blanchet [Tue, 09 Sep 2014 20:51:36 +0200] rev 58273

ported HOL-Proofs-Lambda to new datatypes

isabelle