Even more material from the HOL Light metric space library

Adjustments for the simplified version of real_le_lsqrt

merged

NEWS: Announcing the metric space material

Hiding the constructor names, particularly to avoid conflicts involving "ext"

New HOL Light material on metric spaces and topological spaces

provide scala-3.3.0;

enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;

tuned NEWS;

more NEWS;

NEWS;

removed intro, desc, elim, and simp annotations from FSet lemmas that are…

adapted to Isabelle/84a7a0029c82

merged

set up code generation for fset

NEWS

redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.

merged

tuned signature;

clarified treatment of context;

clarified treatment of context;

more operations;

NEWS

added author

renamed notin_fset to not_fmember

merged

adapted Transfer_Debug from fmember to fempty

renamed variables

fixed lemma name

merged

replaced some lemmas' implicit formulas by explicit ones to avoid silent changes

redefined FSet.fmember as an abbreviation based on Set.member

merged

adapted to Isabelle/0252d635bfb2

merge

Merge with developper version on LISN gut

merge

prefer @{attributes} antiquotation over Attrib.internal;

merged

tuned proofs;

merged

clarified output of embedded values, e.g. for 'print_locale';

more uniform simproc_setup: avoid vacuous abstraction over morphism, which…

proper setup for rule attribute;

tuned;

tuned: more antiquotations;

tuned signature: more position information;

tuned;

Finally, the abstract metric space development

merged

Deleted a superfluous assumption. This proof is a horror

fixed some bibliographic entries

merged

tuned

merged

merged

adapted to current Isabelle/ec1c0daa3fbd;

adapted to Isabelle/5edd5b12017d;

adapted to current Isabelle/ec1c0daa3fbd;

backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;

proper morphism context;

proper morphism context;

adapted to Isabelle/5ab5add88922;

merged

misc tuning and clarification;

tuned signature;

tuned;

tuned --- Token.make_string / Token.assign are value-oriented;

tuned signature;

tuned signature;

more documentation;

more robust context: fail immediately via Morphism.the_theory, instead of…

prefer static simpset;

more operations;

omit pointless morphism in global theory;

more careful treatment of context for method source;

clarified context;

more careful reset_context for stored entity;

remove pointless context setup (see also b2e449c155a4);

clarified signature;

tuned;

more careful reset/set_context for stored declarations;

tuned;

clarified data: avoid pointless Morphism.transform;

clarified signature: more explicit types;

proper Token.Declaration for internal_declaration;

more standard treatment of morphism context;

tuned: avoid duplication;

more standard treatment of morphism context, but hardly relevant here;

more careful treatment of set_context / reset_context for persistent morphisms;

tuned;

tuned signature;

clarified transfer / trim_context on persistent Token.source (e.g. attribute…

proper transfer to supported "bundle ... begin unbundle ... end", e.g. see…

support for context within morphism (for background theory);

clarified signature;

tuned;

clarified stored thm: result from notes;