| Tue, 03 Mar 2009 14:54:12 +0100 | wenzelm | nicer_shortest: use NameSpace.extern_flags with disabled "features" instead of internal NameSpace.get_accesses; | changeset | files |
| Tue, 03 Mar 2009 14:53:29 +0100 | wenzelm | moved name space externalization flags back to name_space.ML; | changeset | files |
| Tue, 03 Mar 2009 14:52:13 +0100 | wenzelm | moved name space externalization flags back to name_space.ML; | changeset | files |
| Tue, 03 Mar 2009 14:16:05 +0100 | wenzelm | reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372); | changeset | files |
| Tue, 03 Mar 2009 14:08:53 +0100 | wenzelm | merged | changeset | files |
| Tue, 03 Mar 2009 14:07:43 +0100 | wenzelm | Thm.binding; | changeset | files |
| Tue, 03 Mar 2009 14:07:23 +0100 | wenzelm | added type binding and val empty_binding; | changeset | files |