Diffusion Isabelle bdb5de00379a

merged
bdb5de00379a
Actions

Tags

None

Subscribers

None

Description

merged

Details

Provenance

Authored on

Parents

rISABELLE515a69e976c3: added author
rISABELLEe30a56be9c7b: merged

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rISABELLEbdb5de00379a: merged.May 8 2023, 5:26 PM

Merged Changes

e30a56be9c7b merged
Author
makarius
Browse Repository
No Builds
No Audits
c1b8fdd6588a tuned comments;
Author
makarius
Browse Repository
No Builds
No Audits
a35b9a01b5a9 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
21cdcd120a78 hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g.
Author
makarius
Browse Repository
No Builds
No Audits
f83702560730 minor performance tuning;
Author
makarius
Browse Repository
No Builds
No Audits
2585ce904bb3 minor performance tuning;
Author
makarius
Browse Repository
No Builds
No Audits
a12c48fbf10f back to more elementary concept of aliases as adhoc change of accesses, but now…
Author
makarius
Browse Repository
No Builds
No Audits
14d133cff073 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
85811617efcd clarified data representation: slightly more compact, since internals_hidden is…
Author
makarius
Browse Repository
No Builds
No Audits
ca11a87bd2c6 more operations;
Author
makarius
Browse Repository
No Builds
No Audits
a7ca67369755 more operations;
Author
makarius
Browse Repository
No Builds
No Audits
93999ffdb9dd more operations;
Author
makarius
Browse Repository
No Builds
No Audits
ab6e4085a19d minor performance tuning;
Author
makarius
Browse Repository
No Builds
No Audits
305a6902abb3 unused;
Author
makarius
Browse Repository
No Builds
No Audits
b256ac9c0577 more complete accesses for "extern" operation, notably for aliases;
Author
makarius
Browse Repository
No Builds
No Audits
31ea5c1f874d more explicit entries for aliases, with proper checks in "strict" mode (e.g.
Author
makarius
Browse Repository
No Builds
No Audits
f68df517e8c4 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
8ce2425a7c94 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
6bb2f9b32804 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
fa3474ed80be unused;
Author
makarius
Browse Repository
No Builds
No Audits
81b953729ff7 minor performance tuning;
Author
makarius
Browse Repository
No Builds
No Audits
d4184ea197ec tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
3a97b5bff51a minor performance tuning;
Author
makarius
Browse Repository
No Builds
No Audits
01e04f024bb5 revert pointless performance tuning fd5f4455e033: no measurable difference in…
Author
makarius
Browse Repository
No Builds
No Audits
93d2b3786959 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
1d82061fbb12 more accurate treatment of traditional name space accesses (refining…
Author
makarius
Browse Repository
No Builds
No Audits
8d905eef9feb tuned;
Author
makarius
Browse Repository
No Builds
No Audits
d7eabea9f837 proper treatment of restriction (for 'qualified');
Author
makarius
Browse Repository
No Builds
No Audits
fda3e9c8a894 misc tuning;
Author
makarius
Browse Repository
No Builds
No Audits
948f5dc4d694 more complete accesses for hide operation (amending fcd85e04a948), e.g.
Author
makarius
Browse Repository
No Builds
No Audits
c4677a6aae2c more standard name bindings (amending 5bf71b4da706): avoid odd full_name like…
Author
makarius
Browse Repository
No Builds
No Audits
8f3204e28783 minor performance tuning: more compact representation of only sparsely table;
Author
makarius
Browse Repository
No Builds
No Audits
fcd85e04a948 minor performance tuning: no storage of accesses, produce Binding.
Author
makarius
Browse Repository
No Builds
No Audits
27b5cb41c253 proper checks;
Author
makarius
Browse Repository
No Builds
No Audits
6c8682291a5d tuned;
Author
makarius
Browse Repository
No Builds
No Audits
5ec51a914f6e tuned structure;
Author
makarius
Browse Repository
No Builds
No Audits
0290a9879b03 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
81e356fd6f60 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
238307775d52 clarified extern vs. alias/hide: output alternative names, if possible;
Author
makarius
Browse Repository
No Builds
No Audits
00c38dd0f30f tuned;
Author
makarius
Browse Repository
No Builds
No Audits
99df2576107f minor performance tuning: more compact, more sharing;
Author
makarius
Browse Repository
No Builds
No Audits
fd5f4455e033 potential performance tuning: more compact data structure, but less sharing;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (3)

Path

Size

src/

HOL/

Library/

Multiset_Order.thy

rISABELLEbdb5de00379a

NEWS

Loading...

src/HOL/Library/Multiset.thy

Loading...

src/HOL/Library/Multiset_Order.thy

Loading...