All Stories
Use Results
Edit Query
Hide Query

Julian Brunner <julianbrunner@gmail.com> committed rAFPd00ccc5a880c: adjusted acceptance conditions.

adjusted acceptance conditions

Julian Brunner <julianbrunner@gmail.com> committed rAFPe77e24b46bdc: significantly reduced amoutn of boilerplate.

significantly reduced amoutn of boilerplate

Julian Brunner <julianbrunner@gmail.com> committed rAFP1ff8d9fa1105: updated DFA and NFA to use intermediate layer.

updated DFA and NFA to use intermediate layer

Julian Brunner <julianbrunner@gmail.com> committed rAFPc163b0235570: adjusted LTL_Master_Theorem for changes in automata library.

adjusted LTL_Master_Theorem for changes in automata library

Julian Brunner <julianbrunner@gmail.com> committed rAFP7dd6d78906a3: added deterministic complementation.

added deterministic complementation

Julian Brunner <julianbrunner@gmail.com> committed rAFP4cb0bfddda9c: refactoring.

refactoring

Julian Brunner <julianbrunner@gmail.com> committed rAFP882b1eceb529: added deterministic path acceptance.

added deterministic path acceptance

Julian Brunner <julianbrunner@gmail.com> committed rAFP2a4d3cb0f059: generalized deterministic degeneralization.

generalized deterministic degeneralization

Julian Brunner <julianbrunner@gmail.com> committed rAFPc3c986158767: renaming for consistency.

renaming for consistency

Julian Brunner <julianbrunner@gmail.com> committed rAFP49e0ab592007: generalized deterministic acceptance test.

generalized deterministic acceptance test

Julian Brunner <julianbrunner@gmail.com> committed rAFPfe4bf27391fd: generalized degeneralization.

generalized degeneralization

Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> committed rAFP61c386d0635b: Increased timeout in ROOT file to avoid fails while building the entry..

Increased timeout in ROOT file to avoid fails while building the entry.

Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> committed rAFP2002acaf36cc: jenkins/job/isabelle-all still reports fail to build because of timeout. Tested….

jenkins/job/isabelle-all still reports fail to build because of timeout. Tested…

Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> committed rAFP6037ad2499b0: Added a couple of lemmas to shorten proofs for convergence in types of class….

Added a couple of lemmas to shorten proofs for convergence in types of class…

Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> committed rAFPf45e96908c95: Tobias Nipkow found the issue. A line in the proof of frechet_vec_nth. Reduced….

Tobias Nipkow found the issue. A line in the proof of frechet_vec_nth. Reduced…

Asta Halkjær From <s144442@student.dtu.dk> committed rAFPe0ffeae3b9c3: Fix inaccurate word choice..

Fix inaccurate word choice.

Julian Brunner <julianbrunner@gmail.com> committed rAFP2da0b337b200: renaming.

renaming

paulson <lp15@cam.ac.uk> committed rAFP890686fa8418: type class "small" inclusions for types "set", "real" and "complex".

type class "small" inclusions for types "set", "real" and "complex"

Julian Brunner <julianbrunner@gmail.com> committed rAFPec727bc82521: added path automata.

added path automata

Julian Brunner <julianbrunner@gmail.com> committed rAFPbb9ca3026763: cleanup.

cleanup

Julian Brunner <julianbrunner@gmail.com> committed rAFP7b3db2da4005: removed unneeded traces.

removed unneeded traces

Julian Brunner <julianbrunner@gmail.com> committed rAFP35132c29d428: generalized acceptance test.

generalized acceptance test

paulson committed rAFP6081d5be8d08: merged.

merged

paulson <lp15@cam.ac.uk> committed rAFPd02b36b86039: ZFC_in_HOL Change history.

ZFC_in_HOL Change history

paulson <lp15@cam.ac.uk> committed rAFP637ea3b47f8c: Fixed a failing proof..

Fixed a failing proof.

paulson <lp15@cam.ac.uk> committed rAFP8a97181d7212: More lemmas, especially about cardinals and the Aleph sequence.

More lemmas, especially about cardinals and the Aleph sequence

paulson <lp15@cam.ac.uk> committed rAFP7393315c7b60: Generalisation of the "small" predicate to arbitrary sets;.

Generalisation of the "small" predicate to arbitrary sets;

paulson committed rAFP85592c2f97b1: merged.

merged

paulson <lp15@cam.ac.uk> committed rAFP589397f68871: Generalisation of order types to arbitrary sets; ordinal exponentiation.

Generalisation of order types to arbitrary sets; ordinal exponentiation

Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFPce989c675f3a: move lemma less_multiset_doubletons.

move lemma less_multiset_doubletons

Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFPb2241741f50f: fix imports.

fix imports

Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFP766bfc31745e: merge.

merge

nipkow committed rAFPddbab58b4c7d: simplified proofs.

simplified proofs

Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFPdc7cc57f1157: Lambda-free orders: restrict totality to one set.

Lambda-free orders: restrict totality to one set

Julian Brunner <julianbrunner@gmail.com> committed rAFP97558303a643: added NBA n-ary union.

added NBA n-ary union

Julian Brunner <julianbrunner@gmail.com> committed rAFPa3d250c96907: added union nodes and finiteness theorems.

added union nodes and finiteness theorems

Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFP8cbd1aadff7c: EPO: adapt totality proof to suit paper.

EPO: adapt totality proof to suit paper

pruvisto committed rAFP0f0adba767a3: adapted to isabelle-dev/e0237f2eb49d.

adapted to isabelle-dev/e0237f2eb49d

Julian Brunner <julianbrunner@gmail.com> committed rAFP8b6582b73697: merged.

merged

nipkow committed rAFP59346dcf3ea8: finally understood that the second implementation is just a very slight….

finally understood that the second implementation is just a very slight…

nipkow committed rAFPd7cc55445292: tuned topics.

tuned topics

Julian Brunner <julianbrunner@gmail.com> committed rAFP8e4020889297: added n-ary NBA intersection.

added n-ary NBA intersection

Feb 11 2020, 7:21 PM · isabelle-release

nipkow committed rAFPdb2fc75a68cc: more topics.

Feb 11 2020

makarius updated the task description for T12: Hosting of Isabelle/AFP after Jun-2020.

makarius committed rISABELLE22158ebde77f: updated for release;.

updated for release;

Feb 11 2020, 5:03 PM

makarius committed rISABELLE8fd1936490bc: tuned;.

tuned;

Feb 11 2020, 3:42 PM

makarius committed rISABELLE2e1b0ee920f5: updated for release;.

updated for release;

Feb 11 2020, 3:42 PM

paulson <lp15@cam.ac.uk> committed rISABELLEd8fb621fea02: some lemmas about the lex ordering on lists, etc..

some lemmas about the lex ordering on lists, etc.

Feb 11 2020, 1:56 PM

makarius added a project to T8: Clarify underlying Mercurial version: isabelle-release.

Feb 11 2020, 10:45 AM · isabelle-release, phabricator-setup

makarius added a comment to T8: Clarify underlying Mercurial version.

Further hints:

Feb 11 2020, 10:44 AM · isabelle-release, phabricator-setup

Feb 10 2020

makarius committed rISABELLE6c52b1d71f8b: proper symbols;.

proper symbols;

Feb 10 2020, 11:04 PM

makarius committed rISABELLE49fb95d04d43: NEWS;.

NEWS;

makarius committed rISABELLEe06ece7a408f: recover from Unicode accident in 4abd07cd034f;.

recover from Unicode accident in 4abd07cd034f;

makarius committed rISABELLE508b4f6431ae: updated for release;.

updated for release;

makarius committed rISABELLE7736b754b37f: NEWS;.

NEWS;

makarius committed rISABELLE182956c8e020: NEWS;.

NEWS;

makarius committed rISABELLEb3954e1387b0: tuned;.

tuned;

Feb 10 2020, 9:25 PM · isabelle-release

makarius added a comment to T12: Hosting of Isabelle/AFP after Jun-2020.

An Atlassian / Bitbucket spokesperson says "there are no plans to remove Hg from SourceTree" (see
https://community.atlassian.com/t5/Bitbucket-articles/What-to-do-with-your-Mercurial-repos-when-Bitbucket-sunsets/ba-p/1155380#M176).

makarius committed rISABELLE66a06a55c00c: tuned;.

tuned;

Feb 10 2020, 9:14 PM

makarius raised the priority of T3: Adapt Isabelle/VSCode to Webview API from Normal to High.

Feb 10 2020, 9:14 PM · isabelle-release

makarius updated the post content for Blog Post: Plan for Isabelle2020 release.

Feb 10 2020, 8:50 PM

makarius triaged T12: Hosting of Isabelle/AFP after Jun-2020 as High priority.

Feb 10 2020, 8:46 PM · isabelle-release

florian.haftmann committed rISABELLE745e518d3d0b: easy abstraction over pointwise bit operations.

easy abstraction over pointwise bit operations

Feb 10 2020, 8:20 AM

florian.haftmann committed rISABELLEf2da99316b86: more rules for natural deduction from inequalities.

more rules for natural deduction from inequalities

Feb 10 2020, 8:20 AM

Feb 9 2020

florian.haftmann committed rISABELLEe83fe2c31088: rule concerning bit (push_bit ...).

rule concerning bit (push_bit ...)

Feb 9 2020, 2:42 PM

florian.haftmann committed rISABELLE7ae4dcf332ae: more lemmas.

more lemmas

Feb 9 2020, 2:42 PM

Feb 8 2020

makarius committed rISABELLE5d5be87330b5: allow to override repository versions at runtime;.

allow to override repository versions at runtime;

Feb 8 2020, 3:25 PM

Feb 7 2020

makarius committed rISABELLE5de8c6d92bd0: follow Phabricator update 2020 Week 5;.

follow Phabricator update 2020 Week 5;

Feb 7 2020, 8:37 PM

Feb 5 2020

florian.haftmann committed rISABELLE572ab9e64e18: simplified logical constructions.

simplified logical constructions

Feb 5 2020, 11:18 PM

florian.haftmann committed rISABELLE1d8e914e04d6: simplified logical constructions.

simplified logical constructions

Feb 5 2020, 11:18 PM

Feb 4 2020

florian.haftmann committed rISABELLEbd9d27ccb3a3: more theorems.

more theorems

Feb 4 2020, 7:08 PM

paulson <lp15@cam.ac.uk> committed rISABELLE89d05db6dd1f: Simplified, generalised version of Constructible due to E. Gunther, M. Pagano….

Simplified, generalised version of Constructible due to E. Gunther, M. Pagano…

Feb 4 2020, 5:19 PM

nipkow committed rISABELLE6a1c1d1ce6ae: tuned.

tuned

Feb 4 2020, 4:37 PM

Feb 3 2020

nipkow committed rISABELLE63b2789259e7: tuned.

tuned

Feb 3 2020, 6:23 PM

nipkow committed rISABELLEc26de1bd7b00: added Interval_Tree.thy.

added Interval_Tree.thy

Feb 3 2020, 6:23 PM

Feb 2 2020

florian.haftmann committed rISABELLE65ffe9e910d4: more specific class assumptions.

more specific class assumptions

Feb 2 2020, 11:27 AM

florian.haftmann committed rISABELLE96d126844adc: more theorems.

more theorems

Feb 2 2020, 11:27 AM

Jan 28 2020

makarius committed rISABELLE839bf7d74fae: ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9);.

ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9);

Jan 28 2020, 8:28 PM

paulson <lp15@cam.ac.uk> committed rISABELLE5385de42f9f4: Tidied up some messy proofs.

Tidied up some messy proofs

Jan 28 2020, 4:01 PM

florian.haftmann committed rISABELLE0bb0cb558bf9: sketches of ideas still to come.

sketches of ideas still to come

florian.haftmann committed rISABELLE554385d4cf59: more theorems.

more theorems

florian.haftmann committed rISABELLE2525e28e4b8b: generalized.

generalized

florian.haftmann committed rISABELLE3887432720a9: tuned.

tuned