- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Yesterday
Yesterday
paulson <lp15@cam.ac.uk> committed rISABELLE1cadc477f644: Even more material from the HOL Light metric space library.
Even more material from the HOL Light metric space library
Wed, May 31
Wed, May 31
paulson <lp15@cam.ac.uk> committed rAFPa0663cd726cc: Adjustments for the simplified version of real_le_lsqrt.
Adjustments for the simplified version of real_le_lsqrt
paulson <lp15@cam.ac.uk> committed rISABELLE8234c42d20e6: NEWS: Announcing the metric space material.
NEWS: Announcing the metric space material
paulson <lp15@cam.ac.uk> committed rISABELLE3d2db8057b9f: Hiding the constructor names, particularly to avoid conflicts involving "ext".
Hiding the constructor names, particularly to avoid conflicts involving "ext"
paulson <lp15@cam.ac.uk> committed rISABELLE24b70433c2e8: New HOL Light material on metric spaces and topological spaces.
New HOL Light material on metric spaces and topological spaces
provide scala-3.3.0;
makarius committed rISABELLE163e4835a8db: enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;.
enable scala-3.3.0, with forced rebuild of Isabelle/Scala and Isabelle/ML;
Tue, May 30
Tue, May 30
Mon, May 29
Mon, May 29
desharna committed rISABELLEe72884b2da04: removed intro, desc, elim, and simp annotations from FSet lemmas that are….
removed intro, desc, elim, and simp annotations from FSet lemmas that are…
Sun, May 28
Sun, May 28
desharna committed rAFPfccdd28b5d84: adapted to Isabelle/84a7a0029c82.
adapted to Isabelle/84a7a0029c82
desharna committed rISABELLE84a7a0029c82: set up code generation for fset.
set up code generation for fset
desharna committed rISABELLE7735645667f0: redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set..
redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.
Sat, May 27
Sat, May 27
clarified treatment of context;
clarified treatment of context;
Fri, May 26
Fri, May 26
desharna committed rISABELLE776f6b85243f: renamed notin_fset to not_fmember.
renamed notin_fset to not_fmember
desharna committed rISABELLE0366e49dab85: adapted Transfer_Debug from fmember to fempty.
adapted Transfer_Debug from fmember to fempty
desharna committed rISABELLEf40bc75b2a3f: replaced some lemmas' implicit formulas by explicit ones to avoid silent changes.
replaced some lemmas' implicit formulas by explicit ones to avoid silent changes
desharna committed rISABELLE0252d635bfb2: redefined FSet.fmember as an abbreviation based on Set.member.
redefined FSet.fmember as an abbreviation based on Set.member
desharna committed rAFP0de1311fe42d: adapted to Isabelle/0252d635bfb2.
adapted to Isabelle/0252d635bfb2
Burkhart Wolff <wolff@lri.fr> committed rAFP380653982dcd: Merge with developper version on LISN gut.
Merge with developper version on LISN gut
Thu, May 25
Thu, May 25
prefer @{attributes} antiquotation over Attrib.internal;
makarius committed rISABELLE2cd7e5518d0d: clarified output of embedded values, e.g. for 'print_locale';.
clarified output of embedded values, e.g. for 'print_locale';
makarius committed rISABELLE4d9349989d94: more uniform simproc_setup: avoid vacuous abstraction over morphism, which….
more uniform simproc_setup: avoid vacuous abstraction over morphism, which…
proper setup for rule attribute;
tuned: more antiquotations;
tuned signature: more position information;
Tue, May 23
Tue, May 23
paulson <lp15@cam.ac.uk> committed rISABELLEcec875dcc59e: Finally, the abstract metric space development.
Finally, the abstract metric space development
paulson <lp15@cam.ac.uk> committed rAFPa664ef80db6a: Deleted a superfluous assumption. This proof is a horror.
Deleted a superfluous assumption. This proof is a horror
paulson <lp15@cam.ac.uk> committed rAFPc17b25e9151c: fixed some bibliographic entries.
fixed some bibliographic entries
Mon, May 22
Mon, May 22
adapted to current Isabelle/ec1c0daa3fbd;
adapted to Isabelle/5edd5b12017d;
adapted to current Isabelle/ec1c0daa3fbd;
backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;
proper morphism context;
makarius added a reverting change for rAFPa8e9b33d75e1: adapted to Isabelle/5ab5add88922;: rAFP88780e621a30: backout a8e9b33d75e1, thanks to Isabelle/f0aca0506531;.
proper morphism context;
adapted to Isabelle/5ab5add88922;
misc tuning and clarification;
makarius committed rISABELLE3fde7a52c650: tuned --- Token.make_string / Token.assign are value-oriented;.
tuned --- Token.make_string / Token.assign are value-oriented;
more documentation;
makarius committed rISABELLEf0aca0506531: more robust context: fail immediately via Morphism.the_theory, instead of….
more robust context: fail immediately via Morphism.the_theory, instead of…
prefer static simpset;
omit pointless morphism in global theory;
more careful treatment of context for method source;
more careful reset_context for stored entity;
remove pointless context setup (see also b2e449c155a4);
clarified signature;
more careful reset/set_context for stored declarations;
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;
makarius committed rISABELLEa71bfc551891: more standard treatment of morphism context, but hardly relevant here;.
more standard treatment of morphism context, but hardly relevant here;
makarius committed rISABELLE11d6a1e62841: more careful treatment of set_context / reset_context for persistent morphisms;.
more careful treatment of set_context / reset_context for persistent morphisms;
makarius committed rISABELLE4e865c45458b: clarified transfer / trim_context on persistent Token.source (e.g. attribute….
clarified transfer / trim_context on persistent Token.source (e.g. attribute…
makarius committed rISABELLE5ab5add88922: proper transfer to supported "bundle ... begin unbundle ... end", e.g. see….
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see…
makarius committed rISABELLEedb195122938: support for context within morphism (for background theory);.
support for context within morphism (for background theory);
clarified signature;
clarified stored thm: result from notes;