Page MenuHomeIsabelle/Phabricator
Feed All Stories

Today

paulson <lp15@cam.ac.uk> committed rISABELLE378593bf5109: Tidying up another of the nominal examples.
Tidying up another of the nominal examples
Tue, Apr 23, 11:26 AM

Yesterday

paulson <lp15@cam.ac.uk> committed rISABELLE34e0ddfc6dcc: More tidying of Nominal proofs.
More tidying of Nominal proofs
Mon, Apr 22, 11:08 PM
nipkow committed rAFPa23e9762512e: added contributor.
added contributor
Mon, Apr 22, 3:01 PM
paulson <lp15@cam.ac.uk> committed rISABELLE022a9c26b14f: Tidied up another messy theory.
Tidied up another messy theory
Mon, Apr 22, 11:45 AM

Sun, Apr 21

paulson <lp15@cam.ac.uk> committed rISABELLE6d56e85f674e: More proof tidying for Nominal.
More proof tidying for Nominal
Sun, Apr 21, 5:32 PM
kappelmann committed rAFP3133b6848037: merged.
merged
Sun, Apr 21, 12:37 PM
kappelmann committed rAFP2a6196e5b347: feat(Transport) add simpler function type introduction rule for extend.
feat(Transport) add simpler function type introduction rule for extend
Sun, Apr 21, 12:37 PM
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…
Sun, Apr 21, 12:37 PM
kappelmann committed rAFPfe57a84f565f: feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems….
feat(ML_Unificaiton) repeated resolution tactics, tactics now proving theorems…
Sun, Apr 21, 12:37 PM
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> committed rAFPf3289a39d4bf: updated:Standard Borel Spaces.
updated:Standard Borel Spaces
Sun, Apr 21, 2:25 AM
paulson <lp15@cam.ac.uk> committed rISABELLEfec5a23017b5: Tidying up more messy proofs.
Tidying up more messy proofs
Sun, Apr 21, 12:03 AM

Sat, Apr 20

Dominique Unruh <hg.yse9he@rwth.unruh.de> committed rAFP22721115789f: Miscellaneous changes to Complex_Bounded_Operators..
Miscellaneous changes to Complex_Bounded_Operators.
Sat, Apr 20, 11:30 PM
paulson <lp15@cam.ac.uk> committed rISABELLEa30a1385f7d0: Starting to tidy HOL-Nominal-Examples.
Starting to tidy HOL-Nominal-Examples
Sat, Apr 20, 1:09 PM
Emin Karayel <me@eminkarayel.de> committed rAFPe3e5ef410780: Frequency_Moments: Add tutorial on pseudorandom objects..
Frequency_Moments: Add tutorial on pseudorandom objects.
Sat, Apr 20, 7:23 AM
Emin Karayel <me@eminkarayel.de> committed rAFP716e68f04275: Universal_Hash_Families: Remove obsolete code..
Universal_Hash_Families: Remove obsolete code.
Sat, Apr 20, 2:47 AM
Emin Karayel <me@eminkarayel.de> committed rAFP6e02e9bc874d: Frequency_Moments, Distributed_Distinct_Elements: Remove obsolete code..
Frequency_Moments, Distributed_Distinct_Elements: Remove obsolete code.
Sat, Apr 20, 1:59 AM
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…
Sat, Apr 20, 1:08 AM

Fri, Apr 19

paulson committed rAFP672eb4689f1a: merged.
merged
Fri, Apr 19, 7:03 PM
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
Fri, Apr 19, 7:03 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP2548b08bc3c4: merge from AFP 2023.
merge from AFP 2023
Fri, Apr 19, 1:31 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP3f3f3b9278b9: merge.
merge
Fri, Apr 19, 1:31 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP00fb7d6558e5: metadata and sitegen for MFOTL_Checker.
metadata and sitegen for MFOTL_Checker
Fri, Apr 19, 1:31 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP25dbc1e991c8: rerun sitegen after merge from AFP 2023.
rerun sitegen after merge from AFP 2023
Fri, Apr 19, 1:31 PM
nipkow committed rAFPdbe1aa3fe16e: New entry: ConcurrentHOL.
New entry: ConcurrentHOL
Fri, Apr 19, 1:31 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPcda88c9fcbf9: new entry: MFOTL_Checker.
new entry: MFOTL_Checker
Fri, Apr 19, 1:31 PM
paulson <lp15@cam.ac.uk> committed rAFP5492883fb017: Uncertainty_Principle sitegen.
Uncertainty_Principle sitegen
Fri, Apr 19, 1:31 PM
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…
Fri, Apr 19, 1:31 PM
traytel committed rAFP51fb7da70175: sitegen for Broadcast_Psi.
sitegen for Broadcast_Psi
Fri, Apr 19, 1:31 PM
traytel committed rAFP31ea85757858: new entry Broadcast_Psi.
new entry Broadcast_Psi
Fri, Apr 19, 1:31 PM
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…
Fri, Apr 19, 1:12 PM
paulson committed rAFPac2384b8b86d: merged.
merged
Fri, Apr 19, 1:12 PM
Ata Keskin <ata.keskin@tum.de> committed rAFPdb43b58419ea: Removed unnecessary theory file 'Doob_Convergence.thy'.
Removed unnecessary theory file 'Doob_Convergence.thy'
Fri, Apr 19, 1:50 AM
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
Fri, Apr 19, 1:43 AM

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
Thu, Apr 18, 5:53 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2024.
Thu, Apr 18, 4:44 PM · isabelle-release
makarius updated the post content for Blog Post: Release Candidates for Isabelle2024.
Thu, Apr 18, 4:35 PM · isabelle-release
makarius updated the post content for Blog Post: Release Candidates for Isabelle2024.
Thu, Apr 18, 3:53 PM · isabelle-release
makarius committed rISABELLE12ce957231e0: back to post-release mode -- after fork point;.
back to post-release mode -- after fork point;
Thu, Apr 18, 3:29 PM
makarius committed rISABELLEe07f29df1c67: Added tag Isabelle2024-RC2 for changeset ef2134570abb.
Added tag Isabelle2024-RC2 for changeset ef2134570abb
Thu, Apr 18, 3:29 PM
makarius committed rISABELLEbc450c8754ef: merged.
merged
Thu, Apr 18, 3:29 PM
paulson <lp15@cam.ac.uk> committed rISABELLEe414bcc5a39e: Acknowledgement of Ata Keskin for his Martingales material.
Acknowledgement of Ata Keskin for his Martingales material
Thu, Apr 18, 2:08 PM
desharna committed rAFPd8aa8cc91178: added equivalence of concepts between First_Order_Terms.Position and HOL….
added equivalence of concepts between First_Order_Terms.Position and HOL…
Thu, Apr 18, 8:55 AM

Wed, Apr 17

makarius committed rISABELLEef2134570abb: merged.
merged
Wed, Apr 17, 11:45 PM
makarius committed rISABELLE68fc6839679e: update to jdk-21.0.3;.
update to jdk-21.0.3;
Wed, Apr 17, 11:45 PM
paulson committed rISABELLE8262d4f63b58: merged.
merged
Wed, Apr 17, 11:11 PM
paulson <lp15@cam.ac.uk> committed rISABELLE601ff5c7cad5: Tidied up horrible archaic proofs.
Tidied up horrible archaic proofs
Wed, Apr 17, 11:11 PM
makarius committed rISABELLE2fe244c4bb01: clarified signature;.
clarified signature;
Wed, Apr 17, 9:47 PM
kappelmann committed rISABELLE39f9084a9668: make adhoc_overloading respect type constraints.
make adhoc_overloading respect type constraints
Wed, Apr 17, 3:05 PM
desharna committed rAFP900cfb1adad1: added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp].
added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp]
Wed, Apr 17, 2:34 PM

Tue, Apr 16

makarius committed rISABELLEb73df63e0f52: merged.
merged
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE761bd2b35217: tuned;.
tuned;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE455ddb251ece: clarified signature;.
clarified signature;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE7e4c3bb3d062: minor performance tuning: avoid redundant server access;.
minor performance tuning: avoid redundant server access;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE66d7a923b750: tuned;.
tuned;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE47f671888a37: tuned;.
tuned;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE05cec0a3c63d: clarified modules and options (from store);.
clarified modules and options (from store);
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE370ebda8bd86: clarified signature;.
clarified signature;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE0323cd9fcab9: clarified signature;.
clarified signature;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE61b8f6ac6860: tuned signature;.
tuned signature;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLEd510a1cf9965: tuned;.
tuned;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLEc188068e41f1: tuned;.
tuned;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLEd4d9a7887b2a: tuned signature;.
tuned signature;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE4b95a1d8b2c9: tuned;.
tuned;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLEc729b1d58982: more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);.
more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
Tue, Apr 16, 5:53 PM
makarius committed rISABELLEf4d3e3915228: tuned messages;.
tuned messages;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLEdbcd6dc7f70f: back to static numa_nodes (reverting part of c2c59de57df9);.
back to static numa_nodes (reverting part of c2c59de57df9);
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE2ac132ee8bf1: tuned;.
tuned;
Tue, Apr 16, 5:53 PM
makarius committed rISABELLE6ec65767d7bd: tuned messages;.
tuned messages;
Tue, Apr 16, 5:53 PM
pruvisto committed rISABELLE247751d25102: canonical time function for List.nth.
canonical time function for List.nth
Tue, Apr 16, 1:30 PM

Mon, Apr 15

paulson committed rISABELLE693d4e6cc5b8: merged.
merged
Mon, Apr 15, 11:25 PM
paulson <lp15@cam.ac.uk> committed rISABELLE2fa018321400: Streamlining of many more archaic proofs.
Streamlining of many more archaic proofs
Mon, Apr 15, 11:25 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE138b5172c7f8: clarified web app parameters: more flexible, using HTML5 id specification….
clarified web app parameters: more flexible, using HTML5 id specification…
Mon, Apr 15, 9:46 PM
Fabian Huch <huch@in.tum.de> committed rAFP7f16aa37c534: proper getopts;.
proper getopts;
Mon, Apr 15, 9:41 PM
Fabian Huch <huch@in.tum.de> committed rAFP2f55893686bc: tuned;.
tuned;
Mon, Apr 15, 9:41 PM
Fabian Huch <huch@in.tum.de> committed rAFP5b2e7d535aff: tuned: use explicit keys;.
tuned: use explicit keys;
Mon, Apr 15, 9:41 PM
nipkow committed rAFP114c5bc73eff: merged.
merged
Mon, Apr 15, 6:05 PM
nipkow committed rAFP95692a54af6b: tuned names.
tuned names
Mon, Apr 15, 6:05 PM
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFP408a29902df3: Removed inactive DOI.
Removed inactive DOI
Mon, Apr 15, 5:48 PM
Thibault Dardinier <thibault.dardinier@inf.ethz.ch> committed rAFPe0dfdf1b8ed4: Removed inactive DOI.
Removed inactive DOI
Mon, Apr 15, 5:48 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd81723aa95cb: added monotonicity lemmas of lex/mul-ext.
added monotonicity lemmas of lex/mul-ext
Mon, Apr 15, 4:53 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd8fb49658d5f: more showl-real instantiation to Show_Real thy.
more showl-real instantiation to Show_Real thy
Mon, Apr 15, 4:15 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1c2509fdeac7: added showl-functions for terms and contexts.
added showl-functions for terms and contexts
Mon, Apr 15, 3:55 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPc61a0a701a26: added many results on first-order terms, added positions.
added many results on first-order terms, added positions
Mon, Apr 15, 1:55 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPa52546d735ec: merge.
merge
Mon, Apr 15, 1:55 PM
Fabian Huch <huch@in.tum.de> committed rAFPeaea08280462: updated docs;.
updated docs;
Mon, Apr 15, 1:31 PM
Fabian Huch <huch@in.tum.de> committed rAFPc34ca8a848b0: proper keys (amending 36cf00eeb9e4);.
proper keys (amending 36cf00eeb9e4);
Mon, Apr 15, 1:17 PM
Fabian Huch <huch@in.tum.de> committed rAFP6539b6f3e1cf: add separate Isabelle tool for metadata editing;.
add separate Isabelle tool for metadata editing;
Mon, Apr 15, 1:17 PM
Fabian Huch <huch@in.tum.de> committed rAFPd2e29e073f08: better defaults;.
better defaults;
Mon, Apr 15, 1:17 PM
Fabian Huch <huch@in.tum.de> committed rAFPbec250baad75: clarified AFP base dir: usually given by environment;.
clarified AFP base dir: usually given by environment;
Mon, Apr 15, 1:17 PM
Fabian Huch <huch@in.tum.de> committed rAFP8fd1acd065c6: activate slow metadata checks by default;.
activate slow metadata checks by default;
Mon, Apr 15, 10:49 AM
Fabian Huch <huch@in.tum.de> committed rAFPbd75044b84f8: fix broken metadata introduced by 20b8a26117af;.
fix broken metadata introduced by 20b8a26117af;
Mon, Apr 15, 10:04 AM

Sun, Apr 14

paulson committed rISABELLEfddf8d9c8083: merged.
merged
Sun, Apr 14, 11:40 PM
paulson <lp15@cam.ac.uk> committed rISABELLE577a2896ace9: More tidying of old proofs.
More tidying of old proofs
Sun, Apr 14, 11:40 PM
paulson <lp15@cam.ac.uk> committed rISABELLE2ff4cc7fa70a: More tidying and removal of "apply".
More tidying and removal of "apply"
Sun, Apr 14, 11:40 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2024.
Sun, Apr 14, 1:24 PM · isabelle-release
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> committed rAFP81de808826f9: updated:Standard_Borel_Spaces.
updated:Standard_Borel_Spaces
Sun, Apr 14, 8:00 AM

Sat, Apr 13

Simon Wimmer <wimmers@in.tum.de> committed rISABELLE7506cb70ecfb: Add subgoals variant of 'sketch' command.
Add subgoals variant of 'sketch' command
Sat, Apr 13, 10:23 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP2db006965e8e: fix document generator: _ -> -.
fix document generator: _ -> -
Sat, Apr 13, 8:03 AM
Michikazu Hirata <hirata.m.ac@m.titech.ac.jp> committed rAFP62f87ac53318: update: Standard_Borel_Spaces.
update: Standard_Borel_Spaces
Sat, Apr 13, 1:35 AM

Fri, Apr 12

paulson committed rISABELLEc111785fd640: merged.
merged
Fri, Apr 12, 11:20 PM