Diffusion Isabelle 125414e23e12

merged
125414e23e12
Actions

Description

merged

Details

Provenance

paulson

Authored on

Parents

rISABELLE71d075d18b6e: simplified a lot of messy proofs
rISABELLE9b8770994780: merged

Branches

Unknown

Tags

Unknown

Event Timeline

paulson committed rISABELLE125414e23e12: merged.Mar 19 2023, 7:55 PM

Merged Changes

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

9b8770994780 merged
Author
desharna
Browse Repository
No Builds
No Audits
58b3913059fa added lemma multp_repeat_mset_repeat_msetI
Author
desharna
Browse Repository
No Builds
No Audits
07e2cafcc97e more operations;
Author
makarius
Browse Repository
No Builds
No Audits
7969fa41439b merged
Author
paulson
Browse Repository
No Builds
No Audits
05329cd9db4b merged
Author
paulson
Browse Repository
No Builds
No Audits
71f001027a13 Proof simplification
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
3e8e749935fc proper "build_thorough" for "isabelle update" (amending 9e5f8f6e58a0);
Author
makarius
Browse Repository
No Builds
No Audits
a76f49a03448 merged
Author
makarius
Browse Repository
No Builds
No Audits
1db732e6c3d2 back to compression in Isabelle/Scala (in contrast to f7174238b5e3), e.g.
Author
makarius
Browse Repository
No Builds
No Audits
bc8e2fec9650 vacuum everything in the database;
Author
makarius
Browse Repository
No Builds
No Audits
e92000492895 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
e7d8e990d378 proper vacuum of session_info tables: only once per build process;
Author
makarius
Browse Repository
No Builds
No Audits
daaaf59375e9 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
649708f75c6f more thorough database checks;
Author
makarius
Browse Repository
No Builds
No Audits
9e5f8f6e58a0 more thorough treatment of build prefs, guarded by system option…
Author
makarius
Browse Repository
No Builds
No Audits
488a48453d74 clarified build options;
Author
makarius
Browse Repository
No Builds
No Audits
08fcde7c55c0 clarified ML option vs. Scala option (see also caa182bdab7a);
Author
makarius
Browse Repository
No Builds
No Audits
34176328fc67 merge conflict
Author
nipkow
Browse Repository
No Builds
No Audits
8a6a79ed5a83 unified function update and map update syntaxes
Author
nipkow
Browse Repository
No Builds
No Audits
b9e9b818d7b0 removed accidental junk
Author
blanchette
Browse Repository
No Builds
No Audits
8f96ac621bfd map update syntax
Author
nipkow
Browse Repository
No Builds
No Audits
5cb7fd36223b proper sorting of result (amending f458547b4f0f);
Author
makarius
Browse Repository
No Builds
No Audits
d15ad84d75f7 merged
Author
makarius
Browse Repository
No Builds
No Audits
a84f0b1f607d enforce rebuild of Isabelle/ML;
Author
makarius
Browse Repository
No Builds
No Audits
74cd42d053bf more operations;
Author
makarius
Browse Repository
No Builds
No Audits
f5d3ade80d15 more specific vacuum operation, which is also relevant to PostgreSQL;
Author
makarius
Browse Repository
No Builds
No Audits
c82d49a56cf9 tuned signature: removed redundant argument;
Author
makarius
Browse Repository
No Builds
No Audits
b45fc98d11ea tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
45bd5c26cbcc proper build_uuid for Build_Process.Task: thus old entries are removed via…
Author
makarius
Browse Repository
No Builds
No Audits
57fdb6c846b0 more informative Build_Process.Snapshot;
Author
makarius
Browse Repository
No Builds
No Audits
d7eb6a4522b8 more explicit snapshot of "_state" and "_database";
Author
makarius
Browse Repository
No Builds
No Audits
4240e9528586 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
a2a4adc268b8 removed redundant State.workers: directly maintained within the database, using…
Author
makarius
Browse Repository
No Builds
No Audits
fd553b54fce1 more thorough cleanup;
Author
makarius
Browse Repository
No Builds
No Audits
136ab737a36d tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
78913f29fc21 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
26bb79d17910 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
5f706f7c624b more thorough synchronization of internal "_state" vs. external "_database";
Author
makarius
Browse Repository
No Builds
No Audits
b7fe1d822dc1 more database content;
Author
makarius
Browse Repository
No Builds
No Audits
b1ca8975490a clarified modules;
Author
makarius
Browse Repository
No Builds
No Audits
739cb777cc75 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
e79a5ce8a74c clarified modules;
Author
makarius
Browse Repository
No Builds
No Audits
c14db5d67400 tuned output;
Author
makarius
Browse Repository
No Builds
No Audits
c55443f9fedd tuned output;
Author
makarius
Browse Repository
No Builds
No Audits
7edbb16bc60f Adjusted to new map update priorities
Author
nipkow
Browse Repository
No Builds
No Audits
48b4e0cd94cd bring priority in line with ordinary function update notation
Author
nipkow
Browse Repository
No Builds
No Audits
4b688b8f1de3 merged
Author
nipkow
Browse Repository
No Builds
No Audits
a28ee8058ea3 use tree (simpler) instead of rbt (exercise)
Author
nipkow
Browse Repository
No Builds
No Audits
4563db765eb2 enforce rebuild of Isabelle/ML;
Author
makarius
Browse Repository
No Builds
No Audits
9ed8b85e7d67 more direct state update;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (1)

Path

Size

src/

HOL/

Complex_Analysis/

Cauchy_Integral_Formula.thy

rISABELLE125414e23e12

View Options

src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy

merged125414e23e12Actions

Description

Details

Event Timeline

Merged Changes

Changes (1)

rISABELLE125414e23e12

src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy

merged
125414e23e12
Actions