| 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 |
| Thu, 23 Nov 2006 00:52:03 +0100 | wenzelm | moved ML syntax operations to structure ML_Syntax; | changeset | files |
| Thu, 23 Nov 2006 00:52:01 +0100 | wenzelm | Basic ML syntax operations. | changeset | files |