Sun, 29 Mar 2009 17:47:58 +0200 | wenzelm | tuned; | changeset | files |
Sun, 29 Mar 2009 17:47:50 +0200 | wenzelm | added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; | changeset | files |
Sun, 29 Mar 2009 16:13:44 +0200 | wenzelm | unified binding prefix terminology; | changeset | files |