| Thu, 28 May 2009 22:57:17 -0700 | huffman | generalize constants in SEQ.thy to class metric_space | changeset | files |
| Tue, 02 Jun 2009 13:15:16 +0200 | wenzelm | early setup of secure operations (again, cf. deddd77112b7) -- NB: fix_ints is required for bootstrap; | changeset | files |
| Mon, 01 Jun 2009 23:28:07 +0200 | wenzelm | structure ML_Compiler; | changeset | files |
| Mon, 01 Jun 2009 23:28:06 +0200 | wenzelm | added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test); | changeset | files |