Search Advanced Search

Advanced Search
Use Results
Edit Query
Hide Query

	Open
	Closed

rAFP25dbc1e991c8: rerun sitegen after merge from AFP 2023
Diffusion Commit
rAFP2548b08bc3c4: merge from AFP 2023
Diffusion Commit
rAFP00fb7d6558e5: metadata and sitegen for MFOTL_Checker
Diffusion Commit
rAFPcda88c9fcbf9: new entry: MFOTL_Checker
Diffusion Commit
rAFPdbe1aa3fe16e: New entry: ConcurrentHOL
Diffusion Commit
rAFP5492883fb017: Uncertainty_Principle sitegen
Diffusion Commit
rAFP4ecda9e9f43b: New entry /Users/lp15/.isabelle/Isabelle2023/browser_info/AFP/Uncertainty_Princ…
Diffusion Commit
rAFP51fb7da70175: sitegen for Broadcast_Psi
Diffusion Commit
rAFP31ea85757858: new entry Broadcast_Psi
Diffusion Commit
rAFPac2384b8b86d: merged
Diffusion Commit
rAFP105bd5da5e7e: Updated KnuthMorrisPratt to include new definitions by Christian Zimmerer using…
Diffusion Commit
rAFPdb43b58419ea: Removed unnecessary theory file 'Doob_Convergence.thy'
Diffusion Commit
rAFP59321c4a59e5: Updated Doob_Convergence to use the newest version of Martingales
Diffusion Commit
rISABELLE0c51e0a6bc37: sketch & explore: recover from duplicate fixed variables in Isar proofs
Diffusion Commit
rISABELLE12ce957231e0: back to post-release mode -- after fork point;
Diffusion Commit
rISABELLEbc450c8754ef: merged
Diffusion Commit
rISABELLEe07f29df1c67: Added tag Isabelle2024-RC2 for changeset ef2134570abb
Diffusion Commit
rISABELLEe414bcc5a39e: Acknowledgement of Ata Keskin for his Martingales material
Diffusion Commit
rAFPd8aa8cc91178: added equivalence of concepts between First_Order_Terms.Position and HOL…
Diffusion Commit
rISABELLEef2134570abb: merged
Diffusion Commit
rISABELLE68fc6839679e: update to jdk-21.0.3;
Diffusion Commit
rISABELLE8262d4f63b58: merged
Diffusion Commit
rISABELLE601ff5c7cad5: Tidied up horrible archaic proofs
Diffusion Commit
rISABELLE2fe244c4bb01: clarified signature;
Diffusion Commit
rISABELLE39f9084a9668: make adhoc_overloading respect type constraints
Diffusion Commit
rAFP900cfb1adad1: added lemmas inj_on_Fun_fun[simp], inj_on_Fun_args[simp], and inj_on_Fun[simp]
Diffusion Commit
rISABELLEb73df63e0f52: merged
Diffusion Commit
rISABELLE761bd2b35217: tuned;
Diffusion Commit
rISABELLE455ddb251ece: clarified signature;
Diffusion Commit
rISABELLE7e4c3bb3d062: minor performance tuning: avoid redundant server access;
Diffusion Commit
rISABELLE66d7a923b750: tuned;
Diffusion Commit
rISABELLE05cec0a3c63d: clarified modules and options (from store);
Diffusion Commit
rISABELLE370ebda8bd86: clarified signature;
Diffusion Commit
rISABELLE47f671888a37: tuned;
Diffusion Commit
rISABELLE0323cd9fcab9: clarified signature;
Diffusion Commit
rISABELLE61b8f6ac6860: tuned signature;
Diffusion Commit
rISABELLEd510a1cf9965: tuned;
Diffusion Commit
rISABELLEd4d9a7887b2a: tuned signature;
Diffusion Commit
rISABELLEc188068e41f1: tuned;
Diffusion Commit
rISABELLE4b95a1d8b2c9: tuned;
Diffusion Commit
rISABELLEc729b1d58982: more robust tmp_file (see also ab07d4cb7d1c and 146468e05dd4);
Diffusion Commit
rISABELLEf4d3e3915228: tuned messages;
Diffusion Commit
rISABELLE2ac132ee8bf1: tuned;
Diffusion Commit
rISABELLEdbcd6dc7f70f: back to static numa_nodes (reverting part of c2c59de57df9);
Diffusion Commit
rISABELLE6ec65767d7bd: tuned messages;
Diffusion Commit
rISABELLE247751d25102: canonical time function for List.nth
Diffusion Commit
rISABELLE693d4e6cc5b8: merged
Diffusion Commit
rISABELLE2fa018321400: Streamlining of many more archaic proofs
Diffusion Commit
rISABELLE138b5172c7f8: clarified web app parameters: more flexible, using HTML5 id specification…
Diffusion Commit
rAFP7f16aa37c534: proper getopts;
Diffusion Commit
rAFP5b2e7d535aff: tuned: use explicit keys;
Diffusion Commit
rAFP2f55893686bc: tuned;
Diffusion Commit
rAFP114c5bc73eff: merged
Diffusion Commit
rAFP95692a54af6b: tuned names
Diffusion Commit
rAFP408a29902df3: Removed inactive DOI
Diffusion Commit
rAFPe0dfdf1b8ed4: Removed inactive DOI
Diffusion Commit
rAFPd81723aa95cb: added monotonicity lemmas of lex/mul-ext
Diffusion Commit
rAFPd8fb49658d5f: more showl-real instantiation to Show_Real thy
Diffusion Commit
rAFP1c2509fdeac7: added showl-functions for terms and contexts
Diffusion Commit
rAFPa52546d735ec: merge
Diffusion Commit
rAFPc61a0a701a26: added many results on first-order terms, added positions
Diffusion Commit
rAFPeaea08280462: updated docs;
Diffusion Commit
rAFPc34ca8a848b0: proper keys (amending 36cf00eeb9e4);
Diffusion Commit
rAFP6539b6f3e1cf: add separate Isabelle tool for metadata editing;
Diffusion Commit
rAFPd2e29e073f08: better defaults;
Diffusion Commit
rAFPbec250baad75: clarified AFP base dir: usually given by environment;
Diffusion Commit
rAFP8fd1acd065c6: activate slow metadata checks by default;
Diffusion Commit
rAFPbd75044b84f8: fix broken metadata introduced by 20b8a26117af;
Diffusion Commit
rISABELLE577a2896ace9: More tidying of old proofs
Diffusion Commit
rISABELLEfddf8d9c8083: merged
Diffusion Commit
rISABELLE2ff4cc7fa70a: More tidying and removal of "apply"
Diffusion Commit
rAFP81de808826f9: updated:Standard_Borel_Spaces
Diffusion Commit
rISABELLE7506cb70ecfb: Add subgoals variant of 'sketch' command
Diffusion Commit
rAFP2db006965e8e: fix document generator: _ -> -
Diffusion Commit
rAFP62f87ac53318: update: Standard_Borel_Spaces
Diffusion Commit
rISABELLEc111785fd640: merged
Diffusion Commit
rISABELLEc06c95576ea9: Tidied some messy proofs
Diffusion Commit
rISABELLE5ed992c47cdc: prefer canonical theorem name for fact collection declarations
Diffusion Commit
rAFPbbd1dc798620: Merged
Diffusion Commit
rAFP20b8a26117af: Updated HyperHoareLogic entry: Additional rules
Diffusion Commit
rAFPf7ec8c203092: tune imports
Diffusion Commit
rAFPc60abfef602f: polished theory
Diffusion Commit
rAFPf5b7116751a9: documented recent changes
Diffusion Commit
rAFP43c62567dc63: documented changes in Show-entry
Diffusion Commit
rAFPb086e875e09b: use new XML-transformer from IsaFoR, developed by A. Yamada
Diffusion Commit
rAFPb95e62c4c808: provide additional argument so that code-generation in SML/Eval does not fail
Diffusion Commit
rAFP8e2e746ba2c0: drop explicit injectivity proof, provide parsers for nat and int instead and…
Diffusion Commit
rISABELLE83fa23ca40e5: merged
Diffusion Commit
rISABELLE0f9cd1a5edbe: Tidying ugly proofs
Diffusion Commit
rAFPf96cdc08e452: clarified check roots module;
Diffusion Commit
rAFP05b5fea0d115: tuned;
Diffusion Commit
rAFP14d24fbe8ffa: tuned error messages;
Diffusion Commit
rISABELLE5af76462e3a5: tuned;
Diffusion Commit
rISABELLEc0d689c4fd15: tweaked time functions for median-of-medians selection in HOL-Data_Structures
Diffusion Commit
rAFP9bff600ba0bc: updated Standard Borel and S-finite measure monad
Diffusion Commit
rAFPa6d153d38d4b: Multirelations_Heterogeneous: added Hoare rules for multirelations
Diffusion Commit
rAFPc60cdb60c99c: tuned proofs: avoid z3 to make it work on arm64-linux;
Diffusion Commit
rAFPb5c20c32ec87: tuned proofs: avoid z3 to make it work on arm64-linux;
Diffusion Commit
rAFPd874320a81ca: tuned proofs: avoid z3 to make it work on arm64-linux;
Diffusion Commit
rAFP31fcd760227c: tuned proofs: avoid z3 to make it work on arm64-linux;
Diffusion Commit

Advanced SearchUse ResultsEdit QueryHide Query

Advanced Search
Use Results
Edit Query
Hide Query