- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Jan 27 2021
Jan 27 2021
makarius committed rISABELLEb310b93563f6: more robust: support other_isabelle.init_settings for build_history before….
more robust: support other_isabelle.init_settings for build_history before…
obsolete (see Isabelle/b8e12e94cfca);
Jan 26 2021
Jan 26 2021
makarius closed T37: macOS app bundle cannot access folders Desktop, Documents, Downloads as Resolved.
It works by using an x86_64-darwin executable that invokes a shell script: the executable is accepted by Apple "Files and Folders" security, while still being able to launch arm64-darwin Java properly.
Jan 25 2021
Jan 25 2021
makarius committed rISABELLEa5998396051e: more robust: defer error in sessions structure to build process;.
more robust: defer error in sessions structure to build process;
makarius moved T37: macOS app bundle cannot access folders Desktop, Documents, Downloads from Backlog to TODO on the isabelle-release board.
makarius added a comment to T37: macOS app bundle cannot access folders Desktop, Documents, Downloads.
See also:
makarius triaged T37: macOS app bundle cannot access folders Desktop, Documents, Downloads as Normal priority.
Jan 24 2021
Jan 24 2021
merged, with minor edits: Admin/PLATFORMS, CONTRIBUTORS;
provide naproche-20210124 (inactive);
Added tag Isabelle2021-RC3 for changeset 02422c9add5e
makarius committed rISABELLEf9c71ce29150: tuned name, e.g. relevant for Naproche-SAD debugging in Isabelle/jEdit;.
tuned name, e.g. relevant for Naproche-SAD debugging in Isabelle/jEdit;
more operations for client connection;
follow stackage update;
fewer warnings, notably in Naproche-SAD;
IDE support for Naproche-SAD;
makarius committed rISABELLE96321006c2d4: suppress bundled Naproche-SAD component: it is in conflict with building the….
suppress bundled Naproche-SAD component: it is in conflict with building the…
more robust etc/settings;
support isabelle components -u and -x;
proper typescript version, required for "vsce package";
proper type constraint;
VSCode extension for official Isabelle release;
makarius committed rISABELLE624c2b98860a: suppress markup for literal tokens with block control symbols, for better….
suppress markup for literal tokens with block control symbols, for better…
makarius committed rISABELLE31fbde3baa97: more systematic java-gui-setup, also for "isabelle jedit" command-line tool;.
more systematic java-gui-setup, also for "isabelle jedit" command-line tool;
clarified documentation concerning macOS Big Sur;
updated to flatlaf-1.0-rc1;
makarius committed rISABELLE96d87b9c2b42: workaround for Big Sur fullscreen mode: better support for JDialog windows (e.g..
workaround for Big Sur fullscreen mode: better support for JDialog windows (e.g.
clarified platforms;
makarius committed rISABELLE5a954fd5f078: clarified app identification, potentially relevant for macOS "defaults";.
clarified app identification, potentially relevant for macOS "defaults";
makarius committed rISABELLEf78a3be79ad1: updated documentation: HIDPI works smoothly thanks to FlatLaf;.
updated documentation: HIDPI works smoothly thanks to FlatLaf;
updated screenshot;
updated for release;
makarius committed rISABELLE5f49f1149c1c: clarified reports before errors: support completion of bibtex entries in….
clarified reports before errors: support completion of bibtex entries in…
proper theory_long_name;
updated screenshots;
makarius added a reverting change for rISABELLE1105c42722dc: back to post-release mode;: rISABELLEd0c8e8ca3505: revert 1105c42722dc on isabelle-release branch;.
makarius committed rISABELLEc98a2f82b950: more robust GUI, notably for Big Sur full-screen where the hypersearch panel….
more robust GUI, notably for Big Sur full-screen where the hypersearch panel…
revert 1105c42722dc on isabelle-release branch;
adjustments for Word_Lib updates
allow instance for nat
Jan 22 2021
Jan 22 2021
nipkow committed rAFP3c9f87745f30: `first` did not have constant time complexity.
`first` did not have constant time complexity
Susannah Mansky <susannahej@gmail.com> committed rAFP944776fde110: Updating Jinja from apply-style to Isar-style.
Updating Jinja from apply-style to Isar-style
Jan 21 2021
Jan 21 2021
more official support for macOS 11.1 Big Sur;
Jan 20 2021
Jan 20 2021
more informative error;
Simon Wimmer <wimmers@in.tum.de> committed rAFP3d82fe267f9a: Monad_Memo_DP add material on BSTs.
Monad_Memo_DP add material on BSTs
Simon Wimmer <wimmers@in.tum.de> committed rAFPc0a61e29529e: Monad_Memo_DP/Optimal_BST move function argmin.
Monad_Memo_DP/Optimal_BST move function argmin
Simon Wimmer <wimmers@in.tum.de> committed rAFP8c71faeab7b8: Optimal_BST: simplify termination proofs.
Optimal_BST: simplify termination proofs
Simon Wimmer <wimmers@in.tum.de> committed rAFP9cebf89c45f7: Monad_Memo_DP: clean proof, remove unused thms, clean tests.
Monad_Memo_DP: clean proof, remove unused thms, clean tests
Simon Wimmer <wimmers@in.tum.de> committed rAFPc5e379424280: Merge updates on dynamic programming.
Merge updates on dynamic programming
Simon Wimmer <wimmers@in.tum.de> committed rAFP0eac2d7a263d: Added example and tuned proof.
Added example and tuned proof
Simon Wimmer <wimmers@in.tum.de> committed rAFP1190a08539dc: Make slice abbreviation input only.
Make slice abbreviation input only
Simon Wimmer <wimmers@in.tum.de> committed rAFPcddd9b09f0d0: Added bellman-ford implementation with detection of negative cycles.
Added bellman-ford implementation with detection of negative cycles
Simon Wimmer <wimmers@in.tum.de> committed rAFP278bc88810fe: Only one definition of path and weight functions.
Only one definition of path and weight functions
Simon Wimmer <wimmers@in.tum.de> committed rAFPdaebb0e27b64: Tuned proof automation.
Tuned proof automation
Simon Wimmer <wimmers@in.tum.de> committed rAFP1171b510ad2a: Finished main theorems on Bellman-Ford.
Finished main theorems on Bellman-Ford
Simon Wimmer <wimmers@in.tum.de> committed rAFP3944d6a35a00: Progress on true shortest paths.
Progress on true shortest paths
Simon Wimmer <wimmers@in.tum.de> committed rAFP67e783e1f268: Fixed sorries.
Fixed sorries
Simon Wimmer <wimmers@in.tum.de> committed rAFPd0819b6e17c9: Closed sorries.
Closed sorries
Simon Wimmer <wimmers@in.tum.de> committed rAFP6c027266d53e: Fixed guess.
Fixed guess
Simon Wimmer <wimmers@in.tum.de> committed rAFP1c40d029c4bd: Cycle detection lemma.
Cycle detection lemma
Simon Wimmer <wimmers@in.tum.de> committed rAFPb9514d50aa5a: Simplified proof.
Simplified proof
Simon Wimmer <wimmers@in.tum.de> committed rAFPe3b9d924eefa: Improved proof of main correctness theorem for BF.
Improved proof of main correctness theorem for BF
Akihisa Yamada <akihisa.yamada@aist.go.jp> committed rAFP471f6ebae9a4: Scott continuity not assuming strictness.
Scott continuity not assuming strictness
Akihisa Yamada <akihisa.yamada@aist.go.jp> committed rAFP7812e4b5109f: updated description.
updated description
Akihisa Yamada <akihisa.yamada@aist.go.jp> committed rAFPa744362b6529: forgotten commits.
forgotten commits
Akihisa Yamada <akihisa.yamada@aist.go.jp> committed rAFP01c79f4098cd: updating entry for LMCS submission.
updating entry for LMCS submission
Jan 19 2021
Jan 19 2021
paulson <lp15@cam.ac.uk> committed rAFP016604dd1cab: tidied a definition and proof.
tidied a definition and proof
Fabian Huch <huch@in.tum.de> committed rAFPc27ff156ee88: fix(scala): Updated code for 2.13.
fix(scala): Updated code for 2.13
Asta Halkjær From <andro.from@gmail.com> committed rAFPb4690943adb9: Updated comment.
Updated comment
Jan 18 2021
Jan 18 2021
clarified versions;
nipkow committed rAFPbfb55826ffc0: New entry Hood_Melville_Queue.
New entry Hood_Melville_Queue