print_locale: expr;

added join, merge_multi('); tuned extend, make, merge;

merge_stamps: merge_lists' with reversed args;

gen_merge_lists;

added gen_merge_lists(') and merge_lists('); removed obsolete generic_extend, generic_merge, extend_list;

gen_merge_lists';

generic_merge;

converted simp lemmas;

tuned;

Extended match_proof to handle abstractions.

tuned;

improved ordering of evaluated elements;

time_use_thy "Locales";

Isar conversion

theory Locales temporarily disabled;

beginnings of actual locale expressions;

improved locale expression syntax;

locale expression import;

import locale expression;

tuned;

added uname; syntax for locale expressions (presently unused);

tuned;

thm "point.defs";

recovered original "make"; added "fields" operation; renamed "derived_defs" to "defs";

renamed "fields" to "flds" (avoid clash with new "fields" operation);

locale expressions;

use tracing function for trace output;

tracing_fn;

added tracing, tracing_fn;

Set.vimage;