Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | ported Induct to new datatypes | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | half-ported Imperative HOL to new datatypes | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | generalized 'datatype' LaTeX antiquotation and added 'codatatype' | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | tuned messages | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | rename_tac'd scripts | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | reverted 83a8570b44bc, which was a misunderstanding | changeset | files |
Tue, 09 Sep 2014 20:51:36 +0200 | blanchet | rename_tac'd script | changeset | files |