general type of delete_tagged_brl; tuned;

most general type of delete/delete_term;

skip_proof: do not require quick_and_dirty in interactive mode;

support "_::foo" sort constraints;

removed unused simple_read_typ; read_typ, TypeExt.typ_of_term: map_sort argument;

added proof_to_theory';

Syntax.typ_of_term: pass intern sort fn;

Syntax.read_typ: pass intern sort fn;

* Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode; * Pure/syntax: "x::_::foo" sort constraints;

theory data: removed obsolete finish method;

data: removed obsolete finish method;

name space for local thms (export cond_extern, qualified); improved internal naming of fixes;

print_state: up to 7 result names;

qualify imported facts; clarified read/cert_element; theory data: removed obsolete finish; tuned;

variant: preserve suffix of underscores (for skolem/internal names etc.);

join_rules RuleCases.save;

tuned declarations;

tuned;

make SML/NJ happy;

added Pure/Isar/rule_context.ML;

gcd_dvd1 and gcd_dvd2 proven simultaneously;

moved lemmas to theory Hilbert_Choice;

tuned; meson lemmas from Tools/meson.ML;

added remdups_rl;

clarified order of merge_lists';

clarified order in gen_merge_lists';

fixed SML/NJ error (!?);

use merge_lists, merge_alists;

Symtab.merge_multi'; tuned;

type variables: clarified "used" vs. "occ";

Library.gen_merge_lists';

clarified locale operations (rename, merge); tuned;

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;