Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | documented extraction plugin | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | made realizer more robust in the face of nesting through functions | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | removed debugging junk | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | renamed ML file and module | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | made datatype realizer plugin work for new-style datatypes with no nesting | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | ported HOL-Proofs-Lambda to new datatypes | changeset | files |