Many changes to entry `Complex_Bounded_Operators`:

back to post-release mode -- after fork point;

Added tag Isabelle2022-RC3 for changeset d704efeb01db

proper base names;

proper cygwin component (see d042947e47a3)

suppress command echo in output;

include openssh for rsync (see also a1c7829ac2de);

provide naproche-20221002;

merged

clarified signature: more operations;

tuned signature;

tuned, following hints by IntelliJ IDEA;

clarified signature, to support external tools like "isabelle narration";

syntactic type classes for signed division operators

tuned proofs

reduce prominence of facts

merge from afp-2021-1

new entry Undirected_Graph_Theory

New entry: Maximum_Segment_Sum

typo

typo

regenerate site;

added missing file

added topic for data management systems;

New entry Safe_Range_RC

clarified signature;

more explanations on the new order prover (based on 10945fc183cd), without…

restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;

added documentation about new order prover

tweaked

tweaked;

adjust Stalnaker_Logic to changes in Epistemic_Logic;

adjusted to distribution

moved relevant theorems from theory Divides to theory Euclidean_Division

remove duplicate code;

amend jenkins ci build;

restructured ci profile into modular ci build system;

restructure afp ci builds (see Isabelle/3c4e373922ca)

more structured proofs

Cosmetic changes.

fixed some theory presentation issues (?)

recover informal "&" from 0c18df79b1c8;

added a couple of structured proofs

More obsolete "unfold" calls

More syntactic cleanup. LaTeX markup working

getting rid of apply (unfold ...)

more modernisation of syntax

Removal of obsolete ASCII syntax

merge from afp-2021-1

regenerate site;

web entry for Stalnaker_Logic

afp site: minor stylistic improvements;

new entry: Stalnaker Logic

clarified options, following f2094906e491;

clarified options;

Comments on theories brought from ZF-Constructible. Shortening fm names

merged

provide missing LaTeX macro, e.g. for AFP/PAC_Checker;

clarified signature;

streamlined division on polynomials

streamlined division on polynomials

adjusted to distribution

Remove fontenc from root.tex to make Ł show in PDF.

Update ROOT...

Appendix with another axiom system as a variant of the proof.

merge from afp-2021-1

adapt to Isabelle@769a7cd5a16a

adjust Lar's contact info as requested

sitegen for Padic_Field

sitegen for Risk_Free_Lending

new entry: Padic_Field

new entry Implicational_Logic

new entry: Risk_Free_Lending

New entry Separation_Logic_Unbounded

added web files

added web files

New entry SCC_Bloemen_Sequential

clarified signature: re-use store/cache from build results;

tuned signature;

proper filter (amending fb4215da4919);

clarified signature: persistent Node.source / Snapshot.source;

more examples;

clarified conditions: no_build is ok for presentation if "all_current" holds;

tuned;

tuned signature;

clarified presentation_sessions: work with partial results;

tuned signature: removed unused operations;

tuned;

tuned comments;

A few more disambiguations, related to locales in CartesianCategory.

Merged

Further disambiguation of facts to address clashes involving ConcreteCategory…

streamlined division on polynomials

streamlined division on polynomials

Complex_Bounded_Operators: Fixed errors in document generation

Complex_Bounded_Operators: Added numerous new lemmas.

Disambiguate sufficiently many facts in locales so as to permit a top-level…

Merged

Fix a typo.