| Sat, 10 Mar 2012 23:00:07 +0100 | wenzelm | clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval; | changeset | files |
| Sat, 10 Mar 2012 22:02:45 +0100 | wenzelm | eliminated dead code; | changeset | files |
| Sat, 10 Mar 2012 21:25:59 +0100 | wenzelm | clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway; | changeset | files |
| Sat, 10 Mar 2012 20:58:40 +0100 | wenzelm | misc tuning and simplification; | changeset | files |
| Sat, 10 Mar 2012 20:02:15 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 10 Mar 2012 19:49:32 +0100 | wenzelm | clarified Pattern.matchess; | changeset | files |