Page MenuHomeIsabelle/Phabricator

Open Tasks

Low (6)

Wishlist (1)

Active Repositories

Recent Activity

Today

Susannah Mansky <susannahej@gmail.com> committed rAFP944776fde110: Updating Jinja from apply-style to Isar-style.
Updating Jinja from apply-style to Isar-style
Fri, Jan 22, 3:38 AM

Yesterday

makarius committed rISABELLE0398f18ec76c: proper hostname;.
proper hostname;
Thu, Jan 21, 6:18 PM
makarius committed rISABELLE13bd167f4d97: more official support for macOS 11.1 Big Sur;.
more official support for macOS 11.1 Big Sur;
Thu, Jan 21, 6:09 PM

Wed, Jan 20

makarius committed rISABELLE68f0bd0c8e87: more informative error;.
more informative error;
Wed, Jan 20, 10:52 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP3d82fe267f9a: Monad_Memo_DP add material on BSTs.
Monad_Memo_DP add material on BSTs
Wed, Jan 20, 7:31 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPc0a61e29529e: Monad_Memo_DP/Optimal_BST move function argmin.
Monad_Memo_DP/Optimal_BST move function argmin
Wed, Jan 20, 7:31 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP8c71faeab7b8: Optimal_BST: simplify termination proofs.
Optimal_BST: simplify termination proofs
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP22a627a8a0e2: Merged.
Merged
Wed, Jan 20, 3:47 PM
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
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPc5e379424280: Merge updates on dynamic programming.
Merge updates on dynamic programming
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPe69090abc053: Merged.
Merged
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP0eac2d7a263d: Added example and tuned proof.
Added example and tuned proof
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP78ceb5a9dbb1: Cleaned.
Cleaned
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP1190a08539dc: Make slice abbreviation input only.
Make slice abbreviation input only
Wed, Jan 20, 3:47 PM
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
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP278bc88810fe: Only one definition of path and weight functions.
Only one definition of path and weight functions
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPdaebb0e27b64: Tuned proof automation.
Tuned proof automation
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPb9ca92c46cd9: Cleaning.
Cleaning
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP1171b510ad2a: Finished main theorems on Bellman-Ford.
Finished main theorems on Bellman-Ford
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP3944d6a35a00: Progress on true shortest paths.
Progress on true shortest paths
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPbd778b1f0c60: Cleaning.
Cleaning
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP67e783e1f268: Fixed sorries.
Fixed sorries
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPd0819b6e17c9: Closed sorries.
Closed sorries
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP6c027266d53e: Fixed guess.
Fixed guess
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFP1c40d029c4bd: Cycle detection lemma.
Cycle detection lemma
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPb9514d50aa5a: Simplified proof.
Simplified proof
Wed, Jan 20, 3:47 PM
Simon Wimmer <wimmers@in.tum.de> committed rAFPe3b9d924eefa: Improved proof of main correctness theorem for BF.
Improved proof of main correctness theorem for BF
Wed, Jan 20, 3:47 PM
nipkow committed rISABELLEbe9b73dfd3e0: added lemmas.
added lemmas
Wed, Jan 20, 9:51 AM
Akihisa Yamada <akihisa.yamada@aist.go.jp> committed rAFP471f6ebae9a4: Scott continuity not assuming strictness.
Scott continuity not assuming strictness
Wed, Jan 20, 3:11 AM
Akihisa Yamada <akihisa.yamada@aist.go.jp> committed rAFP7812e4b5109f: updated description.
updated description
Wed, Jan 20, 3:11 AM
Akihisa Yamada <akihisa.yamada@aist.go.jp> committed rAFPa744362b6529: forgotten commits.
forgotten commits
Wed, Jan 20, 2:27 AM
Akihisa Yamada <akihisa.yamada@aist.go.jp> committed rAFP01c79f4098cd: updating entry for LMCS submission.
updating entry for LMCS submission
Wed, Jan 20, 1:56 AM

Tue, Jan 19

makarius updated the post content for Blog Post: Release Candidates for Isabelle2021.
Tue, Jan 19, 4:39 PM
paulson <lp15@cam.ac.uk> committed rAFP4ae553526864: Merge.
Merge
Tue, Jan 19, 4:20 PM
paulson <lp15@cam.ac.uk> committed rAFP016604dd1cab: tidied a definition and proof.
tidied a definition and proof
Tue, Jan 19, 4:20 PM
Fabian Huch <huch@in.tum.de> committed rAFPc27ff156ee88: fix(scala): Updated code for 2.13.
fix(scala): Updated code for 2.13
Tue, Jan 19, 4:13 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFPb4690943adb9: Updated comment.
Updated comment
Tue, Jan 19, 11:53 AM

Mon, Jan 18

makarius committed rWEBSITEe7fb0c93f72e: tuned;.
tuned;
Mon, Jan 18, 8:19 PM
makarius committed rWEBSITEcf5706747a48: clarified versions;.
clarified versions;
Mon, Jan 18, 8:02 PM
makarius closed T35: Isabelle/jEdit full-screen problem with macOS Big Sur as Resolved.

See Isabelle/96d87b9c2b42: https://isabelle.sketis.net/repos/isabelle-release/rev/96d87b9c2b42

Mon, Jan 18, 7:44 PM · isabelle-release