Page MenuHomeIsabelle/Phabricator

Open Tasks

Normal (6)

Wishlist (4)

Active Repositories

Recent Activity

Today

florian.haftmann committed rISABELLE5ed992c47cdc: prefer canonical theorem name for fact collection declarations.
prefer canonical theorem name for fact collection declarations
Fri, Apr 12, 7:34 PM
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFPbbd1dc798620: Merged.
Merged
Fri, Apr 12, 3:45 PM
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFP20b8a26117af: Updated HyperHoareLogic entry: Additional rules.
Updated HyperHoareLogic entry: Additional rules
Fri, Apr 12, 3:45 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf7ec8c203092: tune imports.
tune imports
Fri, Apr 12, 3:04 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPc60abfef602f: polished theory.
polished theory
Fri, Apr 12, 2:35 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf5b7116751a9: documented recent changes.
documented recent changes
Fri, Apr 12, 12:30 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP43c62567dc63: documented changes in Show-entry.
documented changes in Show-entry
Fri, Apr 12, 12:28 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb95e62c4c808: provide additional argument so that code-generation in SML/Eval does not fail.
provide additional argument so that code-generation in SML/Eval does not fail
Fri, Apr 12, 12:28 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb086e875e09b: use new XML-transformer from IsaFoR, developed by A. Yamada.
use new XML-transformer from IsaFoR, developed by A. Yamada
Fri, Apr 12, 12:28 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP8e2e746ba2c0: drop explicit injectivity proof, provide parsers for nat and int instead and….
drop explicit injectivity proof, provide parsers for nat and int instead and…
Fri, Apr 12, 12:28 PM
paulson <lp15@cam.ac.uk> committed rISABELLE0f9cd1a5edbe: Tidying ugly proofs.
Tidying ugly proofs
Fri, Apr 12, 11:26 AM
paulson committed rISABELLE83fa23ca40e5: merged.
merged
Fri, Apr 12, 11:26 AM
Fabian Huch <huch@in.tum.de> committed rAFPf96cdc08e452: clarified check roots module;.
clarified check roots module;
Fri, Apr 12, 10:39 AM
Fabian Huch <huch@in.tum.de> committed rAFP05b5fea0d115: tuned;.
tuned;
Fri, Apr 12, 10:21 AM
Fabian Huch <huch@in.tum.de> committed rAFP14d24fbe8ffa: tuned error messages;.
tuned error messages;
Fri, Apr 12, 10:21 AM
Fabian Huch <huch@in.tum.de> committed rISABELLE5af76462e3a5: tuned;.
tuned;
Fri, Apr 12, 10:18 AM

Yesterday

pruvisto committed rISABELLEc0d689c4fd15: tweaked time functions for median-of-medians selection in HOL-Data_Structures.
tweaked time functions for median-of-medians selection in HOL-Data_Structures
Thu, Apr 11, 11:07 PM
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> committed rAFP9bff600ba0bc: updated Standard Borel and S-finite measure monad.
updated Standard Borel and S-finite measure monad
Thu, Apr 11, 11:05 AM
Walter Guttmann <walter.guttmann@canterbury.ac.nz> committed rAFPa6d153d38d4b: Multirelations_Heterogeneous: added Hoare rules for multirelations.
Multirelations_Heterogeneous: added Hoare rules for multirelations
Thu, Apr 11, 6:18 AM

Wed, Apr 10

makarius committed rAFPb5c20c32ec87: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 11:47 PM
makarius committed rAFPc60cdb60c99c: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 11:47 PM
makarius committed rAFPd874320a81ca: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 11:47 PM
makarius committed rAFP31fcd760227c: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 11:47 PM
makarius committed rAFPec1c704f4022: tuned proofs: avoid z3 to make it work on arm64-linux;.
tuned proofs: avoid z3 to make it work on arm64-linux;
Wed, Apr 10, 9:37 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP09e32ec351bb: v1.0.1.0.
v1.0.1.0
Wed, Apr 10, 6:04 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFPdf6613b912d9: v1.0.1.0.
v1.0.1.0
Wed, Apr 10, 6:03 PM
makarius committed rISABELLE36389d25d33e: rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04….
rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04…
Wed, Apr 10, 1:23 PM
makarius committed rISABELLE1a9f0159de5b: merged.
merged
Wed, Apr 10, 1:23 PM
paulson <lp15@cam.ac.uk> committed rISABELLE646cd337bb08: Tiny tweaks to proofs.
Tiny tweaks to proofs
Wed, Apr 10, 12:35 PM
Emin Karayel <me@eminkarayel.de> committed rAFP1d9d53077605: Median_Method: Add converse of lemma median_est and simplify (corresponding)….
Median_Method: Add converse of lemma median_est and simplify (corresponding)…
Wed, Apr 10, 5:36 AM

Tue, Apr 9

Asta Halkjær From <andro.from@gmail.com> committed rAFPe687427e5463: New theory..
New theory.
Tue, Apr 9, 7:26 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP311e9541c68c: added external interface for int/rat-poly factorization, i.e., using integer….
added external interface for int/rat-poly factorization, i.e., using integer…
Tue, Apr 9, 3:59 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP05633b57ded4: merge.
merge
Tue, Apr 9, 3:59 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP98b3f6efc0f7: changed definition of square-free-factorization: now [(p1,e1),...,(pn,en)]….
changed definition of square-free-factorization: now [(p1,e1),...,(pn,en)]…
Tue, Apr 9, 3:59 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf1f16c6ba99c: added "showl", a class similar to "show", but using String.literal instead….
added "showl", a class similar to "show", but using String.literal instead…
Tue, Apr 9, 3:59 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPaa8210767115: indent, new lemma "inj_show_nat".
indent, new lemma "inj_show_nat"
Tue, Apr 9, 3:59 PM

Mon, Apr 8

paulson <lp15@cam.ac.uk> committed rISABELLEf7b9179b5029: A bit of new material about type class "infinite", from Eval_FO.
A bit of new material about type class "infinite", from Eval_FO
Mon, Apr 8, 6:20 PM
paulson <lp15@cam.ac.uk> committed rAFP930a033bce55: The "infinite" typeclass.
The "infinite" typeclass
Mon, Apr 8, 6:20 PM
paulson <lp15@cam.ac.uk> committed rAFPa8e7af355b07: Tidied some ugly proofs.
Tidied some ugly proofs
Mon, Apr 8, 4:46 PM

Sun, Apr 7

Yosuke-Ito-345 <glacier345@gmail.com> committed rAFPc9df2bf00af9: Update.
Update
Sun, Apr 7, 11:19 AM