| Thu, 23 Nov 2006 11:24:33 +0100 | aspinall | PGIP: add retractfile. Be stricter in file open/close protocol. | changeset | files |
| Thu, 23 Nov 2006 00:52:23 +0100 | wenzelm | replaced Args.map_values/Element.map_ctxt_values by general morphism application; | changeset | files |
| Thu, 23 Nov 2006 00:52:19 +0100 | wenzelm | moved ML identifiers to structure ML_Syntax; | changeset | files |
| Thu, 23 Nov 2006 00:52:15 +0100 | wenzelm | added morph_ctxt, morph_witness; | changeset | files |
| Thu, 23 Nov 2006 00:52:11 +0100 | wenzelm | replaced map_values by morph_values; | changeset | files |
| Thu, 23 Nov 2006 00:52:07 +0100 | wenzelm | moved string_of_pair/list/option to structure ML_Syntax; | changeset | files |