adapted to Isabelle/c4677a6aae2c;

adapted to Isabelle/c4677a6aae2c;

merged

tuned comments;

tuned;

minor performance tuning;

hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g.

back to more elementary concept of aliases as adhoc change of accesses, but now…

minor performance tuning;

clarified data representation: slightly more compact, since internals_hidden is…

tuned;

more operations;

more operations;

more operations;

more complete accesses for "extern" operation, notably for aliases;

minor performance tuning;

unused;

tuned;

more explicit entries for aliases, with proper checks in "strict" mode (e.g.

clarified signature;

tuned;

unused;

tuned signature;

minor performance tuning;

minor performance tuning;

revert pointless performance tuning fd5f4455e033: no measurable difference in…

tuned;

more accurate treatment of traditional name space accesses (refining…

tuned;

more standard name bindings (amending 5bf71b4da706): avoid odd full_name like…

proper treatment of restriction (for 'qualified');

more complete accesses for hide operation (amending fcd85e04a948), e.g.

misc tuning;

minor performance tuning: no storage of accesses, produce Binding.

proper checks;

minor performance tuning: more compact representation of only sparsely table;

tuned;

tuned structure;

tuned signature;

tuned;

tuned;

clarified extern vs. alias/hide: output alternative names, if possible;

minor performance tuning: more compact, more sharing;

potential performance tuning: more compact data structure, but less sharing;

Importation of additional lemmas from metric.ml

fixes esp to theory presentation

new material ported from HOL Light's metric.ml

merged

Two new theories containing material ported from HOL Light about abstract…

merged

streamlined

merged

A few new theorems

More new theorems, and a necessary correction

merged

merged

merged

Numerous significant simplifications

merged

tuned

stripped unused functionality

case translation in intermediate language eliminates semantic clone

minor performance tuning;

more correct type calculation

Backed out changeset 5016262a2384

added lemma

thingol: fix abstraction return types in case

merged

tuned; avoided intermediate list and list traversal

tuned; avoided intermediate lists

tuned; avoided intermediate lists

tuned; avoided intermediate list

made 'primcorec' more robust

performance tuning: more balanced time vs. space tradeoff, notably for datatype…

tuned signature;

Some hyphens that should be en dashes

slightly refine WPO-definition

more operations for lexicographic ordering;

tuned;

more operations: following Library list operations and Ord_List.T operations;

tuned;

tuned: concise combinators instead of bulky case-expressions;

provide ML antiquotation "if_none": non-strict version of "the_default";

merged

tuned;

more operations;

proper Thm.trim_context / Thm.transfer (see also 0d401f874942);

more uniform operations wrt. Thm.full_prop_of;

more operations;

proper Thm.trim_context / Thm.transfer for context data;

tuned: more concise data record;

tuned;

tuned signature;

support n-ary merge theory data;

clarified counters and types;

proper theory_long_name;

tuned;

tuned;

prefer theory_long_name in data;