Diffusion Isabelle aca0b615ec4f

merged
aca0b615ec4f
Actions

Description

merged

Details

Provenance

paulson

Authored on

Parents

rISABELLE84a09beb682d: merged
rISABELLE69ee23f83884: merged

Branches

Unknown

Tags

Unknown

Event Timeline

paulson committed rISABELLEaca0b615ec4f: merged.Apr 12 2023, 1:00 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

faaff590bd9e stripped unused functionality
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f041d5060892 tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
b41c8fce442d case translation in intermediate language eliminates semantic clone
Author
florian.haftmann
Browse Repository
No Builds
No Audits
07e82441c19e minor performance tuning;
Author
makarius
Browse Repository
No Builds
No Audits
55fb4572e062 more correct type calculation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
909efe20ff3b Backed out changeset 5016262a2384
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d28dcd57d2f3 added lemma
Author
nipkow
Browse Repository
No Builds
No Audits
5016262a2384 thingol: fix abstraction return types in case
Author
stuebinm <stuebinm@disroot.org>
Browse Repository
No Builds
No Audits
1249dadc9506 merged
Author
desharna
Browse Repository
No Builds
No Audits
8734ca279e59 tuned; avoided intermediate lists
Author
desharna
Browse Repository
No Builds
No Audits
55b81d14a1b8 tuned; avoided intermediate list and list traversal
Author
desharna
Browse Repository
No Builds
No Audits
a1abcf46eb24 tuned; avoided intermediate lists
Author
desharna
Browse Repository
No Builds
No Audits
ce09ea4c0f93 tuned; avoided intermediate list
Author
desharna
Browse Repository
No Builds
No Audits
64beebac04b8 made 'primcorec' more robust
Author
blanchette
Browse Repository
No Builds
No Audits
5aae99b191eb performance tuning: more balanced time vs. space tradeoff, notably for datatype…
Author
makarius
Browse Repository
No Builds
No Audits
019186a60c84 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
430e6c477ba4 more operations for lexicographic ordering;
Author
makarius
Browse Repository
No Builds
No Audits
b83a561086d3 more operations: following Library list operations and Ord_List.T operations;
Author
makarius
Browse Repository
No Builds
No Audits
10c09fb5a874 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
6fcf3ca93dab tuned;
Author
makarius
Browse Repository
No Builds
No Audits
a6bd716a6124 tuned: concise combinators instead of bulky case-expressions;
Author
makarius
Browse Repository
No Builds
No Audits
ee9785abbcd6 provide ML antiquotation "if_none": non-strict version of "the_default";
Author
makarius
Browse Repository
No Builds
No Audits
9c5e8460df05 merged
Author
makarius
Browse Repository
No Builds
No Audits
acee6c7fafff proper Thm.trim_context / Thm.transfer (see also 0d401f874942);
Author
makarius
Browse Repository
No Builds
No Audits
e7fd273657f1 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
38d0a90e87c1 more operations;
Author
makarius
Browse Repository
No Builds
No Audits
01d6b2a44df8 more operations;
Author
makarius
Browse Repository
No Builds
No Audits
5728d5ebce34 more uniform operations wrt. Thm.full_prop_of;
Author
makarius
Browse Repository
No Builds
No Audits
42214742b44a proper Thm.trim_context / Thm.transfer for context data;
Author
makarius
Browse Repository
No Builds
No Audits
c6fcf32010d1 tuned: more concise data record;
Author
makarius
Browse Repository
No Builds
No Audits
b03c64699af0 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
ff924ce0c599 clarified counters and types;
Author
makarius
Browse Repository
No Builds
No Audits
a9626bcb0c3b tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
655bd3b0671b support n-ary merge theory data;
Author
makarius
Browse Repository
No Builds
No Audits
186bd4012b78 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
dfc1db3f0fcb tuned;
Author
makarius
Browse Repository
No Builds
No Audits
44d845b15214 proper theory_long_name;
Author
makarius
Browse Repository
No Builds
No Audits
f4cd6e3b5075 prefer theory_long_name in data;
Author
makarius
Browse Repository
No Builds
No Audits
26d49c15bff0 proper theory_long_name;
Author
makarius
Browse Repository
No Builds
No Audits
5db014c36f42 clarified signature: explicitly distinguish theory_base_name vs.
Author
makarius
Browse Repository
No Builds
No Audits
3c837f8c8ed5 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
dae8b7a9a89a more operations, following Isabelle/ML conventions;
Author
makarius
Browse Repository
No Builds
No Audits
f11bfc151672 clarified theory_id: plain value without state;
Author
makarius
Browse Repository
No Builds
No Audits
89676df5846a tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
0e054e6e7f5e clarified terminology
Author
florian.haftmann
Browse Repository
No Builds
No Audits
2cd00c4054ab minor performance tuning: recursive check of pointer_eq;
Author
makarius
Browse Repository
No Builds
No Audits
bb7238e7d2d9 minor performance tuning: avoid excessive (de)constructions for base cases;
Author
makarius
Browse Repository
No Builds
No Audits
560bdb9f2101 unused (see also 864c7c684651 and b6aa5eac0a1a);
Author
makarius
Browse Repository
No Builds
No Audits
41f1fd0fdb80 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
dd222e2af01a tuned;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (1)

Path

Size

src/

HOL/

Analysis/

Homotopy.thy

rISABELLEaca0b615ec4f

View Options

src/HOL/Analysis/Homotopy.thy

mergedaca0b615ec4fActions

Description

Details

Event Timeline

Merged Changes

Changes (1)

rISABELLEaca0b615ec4f

src/HOL/Analysis/Homotopy.thy

merged
aca0b615ec4f
Actions