Open Tasks
Open Tasks
Normal (6)
Normal (6)
- Nov 27 2021, 3:30 PM
Low (5)
Low (5)
Wishlist (4)
Wishlist (4)
Active Repositories
Active Repositories
Recent Activity
Recent Activity
Today
Today
update Windows build host;
proper command-line;
paulson <lp15@cam.ac.uk> committed rISABELLE378593bf5109: Tidying up another of the nominal examples.
Tidying up another of the nominal examples
Yesterday
Yesterday
paulson <lp15@cam.ac.uk> committed rISABELLE34e0ddfc6dcc: More tidying of Nominal proofs.
More tidying of Nominal proofs
paulson <lp15@cam.ac.uk> committed rISABELLE022a9c26b14f: Tidied up another messy theory.
Tidied up another messy theory
Sun, Apr 21
Sun, Apr 21
paulson <lp15@cam.ac.uk> committed rISABELLE6d56e85f674e: More proof tidying for Nominal.
More proof tidying for Nominal
kappelmann committed rAFP2a6196e5b347: feat(Transport) add simpler function type introduction rule for extend.
feat(Transport) add simpler function type introduction rule for extend
kappelmann committed rAFP237996782d80: feat(Transport) functions as binary relations, improved mono notation, make non….
feat(Transport) functions as binary relations, improved mono notation, make non…
kappelmann committed rAFPfe57a84f565f: feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems….
feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems…
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> committed rAFPf3289a39d4bf: updated:Standard Borel Spaces.
updated:Standard Borel Spaces
paulson <lp15@cam.ac.uk> committed rISABELLEfec5a23017b5: Tidying up more messy proofs.
Tidying up more messy proofs
Sat, Apr 20
Sat, Apr 20
Dominique Unruh <hg.yse9he@rwth.unruh.de> committed rAFP22721115789f: Miscellaneous changes to Complex_Bounded_Operators..
Miscellaneous changes to Complex_Bounded_Operators.
paulson <lp15@cam.ac.uk> committed rISABELLEa30a1385f7d0: Starting to tidy HOL-Nominal-Examples.
Starting to tidy HOL-Nominal-Examples
Emin Karayel <me@eminkarayel.de> committed rAFPe3e5ef410780: Frequency_Moments: Add tutorial on pseudorandom objects..
Frequency_Moments: Add tutorial on pseudorandom objects.
Emin Karayel <me@eminkarayel.de> committed rAFP716e68f04275: Universal_Hash_Families: Remove obsolete code..
Universal_Hash_Families: Remove obsolete code.
Emin Karayel <me@eminkarayel.de> committed rAFP6e02e9bc874d: Frequency_Moments, Distributed_Distinct_Elements: Remove obsolete code..
Frequency_Moments, Distributed_Distinct_Elements: Remove obsolete code.
Emin Karayel <me@eminkarayel.de> committed rAFP1b546d918c0c: Finite_Fields, Universal_Hash_Families, Concentration_Inequalities: Add various….
Finite_Fields, Universal_Hash_Families, Concentration_Inequalities: Add various…
Fri, Apr 19
Fri, Apr 19
paulson <lp15@cam.ac.uk> committed rAFP8bc05281a185: Exchanged the while-loop and tail-recursive versions of the definitions.
Exchanged the while-loop and tail-recursive versions of the definitions
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP2548b08bc3c4: merge from AFP 2023.
merge from AFP 2023
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP3f3f3b9278b9: merge.
merge
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP00fb7d6558e5: metadata and sitegen for MFOTL_Checker.
metadata and sitegen for MFOTL_Checker
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP25dbc1e991c8: rerun sitegen after merge from AFP 2023.
rerun sitegen after merge from AFP 2023
nipkow committed rAFPdbe1aa3fe16e: New entry: ConcurrentHOL.
New entry: ConcurrentHOL
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPcda88c9fcbf9: new entry: MFOTL_Checker.
new entry: MFOTL_Checker
paulson <lp15@cam.ac.uk> committed rAFP5492883fb017: Uncertainty_Principle sitegen.
Uncertainty_Principle sitegen
paulson <lp15@cam.ac.uk> committed rAFP4ecda9e9f43b: New entry /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Uncertainty_Princ….
New entry /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Uncertainty_Princ…
sitegen for Broadcast_Psi
new entry Broadcast_Psi
paulson <lp15@cam.ac.uk> committed rAFP105bd5da5e7e: Updated KnuthMorrisPratt to include new definitions by Christian Zimmerer using….
Updated KnuthMorrisPratt to include new definitions by Christian Zimmerer using…
Ata Keskin <ata.keskin@tum.de> committed rAFPdb43b58419ea: Removed unnecessary theory file 'Doob_Convergence.thy'.
Removed unnecessary theory file 'Doob_Convergence.thy'
Ata Keskin <ata.keskin@tum.de> committed rAFP59321c4a59e5: Updated Doob_Convergence to use the newest version of Martingales.
Updated Doob_Convergence to use the newest version of Martingales
Thu, Apr 18
Thu, Apr 18
Simon Wimmer <wimmers@in.tum.de> committed rISABELLE0c51e0a6bc37: sketch & explore: recover from duplicate fixed variables in Isar proofs.
sketch & explore: recover from duplicate fixed variables in Isar proofs
back to post-release mode -- after fork point;