Page MenuHomeIsabelle/Phabricator
Feed All Stories

Today

nipkow committed rISABELLE03695eeabdde: merged.
merged
Tue, Mar 31, 5:29 PM
nipkow committed rISABELLE07bec530f02e: cleaned proofs.
cleaned proofs
Tue, Mar 31, 5:29 PM

Yesterday

Julian Brunner <julianbrunner@gmail.com> committed rAFPddaf86ffa226: merged.
merged
Mon, Mar 30, 9:29 PM
Julian Brunner <julianbrunner@gmail.com> committed rAFP744b282fd492: updated benchmarks.
updated benchmarks
Mon, Mar 30, 9:29 PM
Julian Brunner <julianbrunner@gmail.com> committed rAFP819a553f7508: using proper atomic propositions, added more benchmarks.
using proper atomic propositions, added more benchmarks
Mon, Mar 30, 9:29 PM
traytel committed rAFPbde08698d726: avoid nonterminal clash in syntax translation.
avoid nonterminal clash in syntax translation
Mon, Mar 30, 9:02 PM
makarius committed rISABELLEc1bc38327bc2: clarified signature;.
clarified signature;
Mon, Mar 30, 8:57 PM
makarius committed rISABELLE3f02bc5a5a03: more accurate treatment of errors;.
more accurate treatment of errors;
Mon, Mar 30, 8:57 PM
makarius committed rISABELLE50425e4c3910: clarified modules: global quasi-scope for markers;.
clarified modules: global quasi-scope for markers;
Mon, Mar 30, 8:57 PM
nipkow committed rISABELLE2e8f861d21d4: redunant simp rule.
redunant simp rule
Mon, Mar 30, 10:35 AM
paulson committed rISABELLE1f957615cae6: merged.
merged
Mon, Mar 30, 1:10 AM
paulson <lp15@cam.ac.uk> committed rISABELLE2a24c2015a61: more ugly old proofs.
more ugly old proofs
Mon, Mar 30, 1:10 AM

Sun, Mar 29

makarius committed rISABELLE4c8edd527940: merged.
merged
Sun, Mar 29, 10:52 PM
makarius committed rISABELLE189f17479275: tuned;.
tuned;
Sun, Mar 29, 10:52 PM
makarius committed rISABELLEf0499449e149: clarified modules;.
clarified modules;
Sun, Mar 29, 10:52 PM
makarius committed rISABELLEb3bddebe44ca: clarified signature: more explicit type Protocol_Message.Marker;.
clarified signature: more explicit type Protocol_Message.Marker;
Sun, Mar 29, 10:52 PM
makarius committed rISABELLEab5009192ebb: tuned signature -- follow Scala;.
tuned signature -- follow Scala;
Sun, Mar 29, 10:52 PM
makarius committed rISABELLE281591ab169b: tuned;.
tuned;
Sun, Mar 29, 10:52 PM
makarius committed rISABELLE5a4ccef7f310: more explicit type Protocol_Message.Marker;.
more explicit type Protocol_Message.Marker;
Sun, Mar 29, 10:52 PM
makarius committed rISABELLEe33f6e5f86b6: clarified protocol messages: explicitly use physical_writeln, always….
clarified protocol messages: explicitly use physical_writeln, always…
Sun, Mar 29, 10:52 PM
makarius committed rISABELLE1b8861bcb03c: tuned;.
tuned;
Sun, Mar 29, 10:52 PM
makarius committed rISABELLE01166f13c2c0: tuned whitespace;.
tuned whitespace;
Sun, Mar 29, 10:52 PM
paulson <lp15@cam.ac.uk> committed rISABELLEa9de39608b1a: more tidying up of old apply-proofs.
more tidying up of old apply-proofs
Sun, Mar 29, 6:37 PM

Sat, Mar 28

makarius committed rISABELLE74c874b5aed0: merged.
merged
Sat, Mar 28, 10:05 PM
makarius committed rISABELLEe6dead7d5334: tuned;.
tuned;
Sat, Mar 28, 10:05 PM
makarius committed rISABELLE6bce25f9d0ab: tuned;.
tuned;
Sat, Mar 28, 10:05 PM
makarius committed rISABELLEe0a5d6068141: tuned;.
tuned;
Sat, Mar 28, 10:05 PM
makarius committed rISABELLEfb6953e77000: eliminated pointless flag (see also 6533ceee4cd7);.
eliminated pointless flag (see also 6533ceee4cd7);
Sat, Mar 28, 10:05 PM
makarius committed rISABELLE5730eb952208: tuned;.
tuned;
Sat, Mar 28, 10:05 PM
paulson committed rISABELLEbeef2e221c26: merged.
merged
Sat, Mar 28, 9:30 PM
paulson <lp15@cam.ac.uk> committed rISABELLE856c68ab6f13: structured a lot of ancient, horrible proofs.
structured a lot of ancient, horrible proofs
Sat, Mar 28, 9:30 PM
makarius committed rISABELLEd97f504c8145: clarified Isabelle_Process phases;.
clarified Isabelle_Process phases;
Sat, Mar 28, 2:07 PM
makarius committed rISABELLEb3b0d87edd20: clarified order: update syslog before handling exit;.
clarified order: update syslog before handling exit;
Sat, Mar 28, 2:07 PM
makarius committed rISABELLEf7a652732f4e: tuned error message;.
tuned error message;
Sat, Mar 28, 2:07 PM
makarius committed rISABELLEc6fa217c9d5e: clarified signature: more robust startup_join;.
clarified signature: more robust startup_join;
Sat, Mar 28, 2:07 PM
pruvisto committed rAFP81ec186eae5e: Fixed some typos in Furstenberg_Topology.
Fixed some typos in Furstenberg_Topology
Sat, Mar 28, 12:15 PM
kleing committed rAFP9ff984debb46: merge from afp-2019.
merge from afp-2019
Sat, Mar 28, 6:13 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd67fe5c0503b: website update.
website update
Sat, Mar 28, 6:13 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP4c1cafe5bbdb: new entry: Furtenberg Topology.
new entry: Furtenberg Topology
Sat, Mar 28, 6:13 AM
nipkow committed rAFP7b6e642f98f1: New entry WOOT_Strong_Eventual_Consistency.
New entry WOOT_Strong_Eventual_Consistency
Sat, Mar 28, 6:13 AM
paulson <lp15@cam.ac.uk> committed rAFP50666eed97fe: Relational-Incorrectness-Logic website.
Relational-Incorrectness-Logic website
Sat, Mar 28, 6:13 AM
paulson <lp15@cam.ac.uk> committed rAFP270aae5bd0ac: new entry Relational-Incorrectness-Logic.
new entry Relational-Incorrectness-Logic
Sat, Mar 28, 6:13 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb7b8b652815d: added new entry Hello_World.
added new entry Hello_World
Sat, Mar 28, 6:13 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf240cf67fc1f: sitegen + fix of ROOT file.
sitegen + fix of ROOT file
Sat, Mar 28, 6:13 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPe87057e759a5: sitegen.
sitegen
Sat, Mar 28, 6:13 AM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPad98c97b528c: new submission: VeriComp.
new submission: VeriComp
Sat, Mar 28, 6:13 AM
nipkow committed rAFP0b92dd22ffb1: New entry: Goodstein_Lambda.
New entry: Goodstein_Lambda
Sat, Mar 28, 6:13 AM

Fri, Mar 27

makarius committed rISABELLE8e0eece7058d: merged.
merged
Fri, Mar 27, 10:15 PM
makarius committed rISABELLE97ccf48c2f0c: misc tuning based on hints by IntelliJ IDEA;.
misc tuning based on hints by IntelliJ IDEA;
Fri, Mar 27, 10:15 PM
makarius committed rISABELLEd5502ee7c141: tuned;.
tuned;
Fri, Mar 27, 10:15 PM
makarius committed rISABELLE64aad1e46f98: clarified signature;.
clarified signature;
Fri, Mar 27, 10:15 PM
makarius committed rISABELLE23d0a45a9283: clarified signature;.
clarified signature;
Fri, Mar 27, 10:15 PM
makarius committed rISABELLE269dc4bf1f40: clarified signature;.
clarified signature;
Fri, Mar 27, 10:15 PM
makarius committed rISABELLEd025735a4090: clarified signature;.
clarified signature;
Fri, Mar 27, 10:15 PM
makarius committed rISABELLE817e26a03198: tuned;.
tuned;
Fri, Mar 27, 10:15 PM
makarius committed rISABELLE01d92325ddab: clarified signature: more accurate session_base_info.sessions_structure;.
clarified signature: more accurate session_base_info.sessions_structure;
Fri, Mar 27, 10:15 PM
makarius committed rISABELLE8a298184f3f9: clarified signature;.
clarified signature;
Fri, Mar 27, 10:15 PM
nipkow committed rISABELLE71579bd59cd4: added lemma.
added lemma
Fri, Mar 27, 2:29 PM

Wed, Mar 25

paulson <lp15@cam.ac.uk> committed rISABELLE8e4d542f041b: updated to more modern style.
updated to more modern style
Wed, Mar 25, 3:05 PM
paulson committed rISABELLE0c6d29145881: merged.
merged
Wed, Mar 25, 3:05 PM

Tue, Mar 24

paulson <lp15@cam.ac.uk> committed rAFPdeab09fedc87: Grant acknowledgement for ALEXANDRIA (ERC Project 742178).
Grant acknowledgement for ALEXANDRIA (ERC Project 742178)
Tue, Mar 24, 4:04 PM
makarius added a comment to T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow.

We can certainly discuss self-hosting of the Zulip platform (or alternatives), but I personally don't want to be in a "cool place" at all.

Tue, Mar 24, 1:25 PM
lukasstevens added a comment to T9: Evaluate https://discourse.org as replacement for mailman, stackoverflow.

With the current situation leading to increased activity at https://isabelle.zulipchat.com, it would be a good opportunity to discuss a switch to Zulipchat some time after the Isabelle2020 release.

Tue, Mar 24, 12:09 PM
Asta Halkjær From <s144442@student.dtu.dk> committed rAFP8e310d6353b2: Update websites and emails..
Update websites and emails.
Tue, Mar 24, 10:43 AM
Asta Halkjær From <s144442@student.dtu.dk> committed rAFPc00714f311dc: Update abstract.
Update abstract
Tue, Mar 24, 10:43 AM

Mon, Mar 23

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP057bf095850f: improved estimation by getting rid of max-1 operation in….
improved estimation by getting rid of max-1 operation in…
Mon, Mar 23, 8:31 PM
makarius committed rISABELLEd1c2ff90c29a: updated to scala-2.12.11;.
updated to scala-2.12.11;
Mon, Mar 23, 4:35 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2020.
Mon, Mar 23, 1:53 PM
makarius updated the post content for Blog Post: Release Candidates for Isabelle2020.
Mon, Mar 23, 1:43 PM
paulson committed rISABELLE5d1370b32975: merged.
merged
Mon, Mar 23, 12:59 PM
paulson <lp15@cam.ac.uk> committed rISABELLEf3fe59e61f3d: put back Nat.le_diff_conv2 because AUTO2 doesn't work with Groups.le_diff_conv2.
put back Nat.le_diff_conv2 because AUTO2 doesn't work with Groups.le_diff_conv2
Mon, Mar 23, 12:59 PM
paulson committed rISABELLE3904cfde1aa9: merged.
merged
Mon, Mar 23, 12:59 PM
paulson <lp15@cam.ac.uk> committed rISABELLE4b1021677f15: tidying up some horrible proofs.
tidying up some horrible proofs
Mon, Mar 23, 12:59 PM
paulson <lp15@cam.ac.uk> committed rISABELLEe30dbfa53b0d: new-style Greater lemmas.
new-style Greater lemmas
Mon, Mar 23, 12:59 PM
paulson <lp15@cam.ac.uk> committed rAFP4424bf5e28e0: more fixes for alias issues (which for Auto2 means giving up).
more fixes for alias issues (which for Auto2 means giving up)
Mon, Mar 23, 12:37 PM

Sun, Mar 22

makarius committed rISABELLE73d1dc57215f: avoid jdk-11.0.6+10: it shows problem "S8217731: Font rendering and glyph….
avoid jdk-11.0.6+10: it shows problem "S8217731: Font rendering and glyph…
Sun, Mar 22, 10:25 PM
paulson <lp15@cam.ac.uk> committed rAFP6bdf58e7175e: elimination of some aliases.
elimination of some aliases
Sun, Mar 22, 9:38 PM
paulson <lp15@cam.ac.uk> committed rAFP9bd18ac101a7: elimination of some aliases, etc..
elimination of some aliases, etc.
Sun, Mar 22, 8:06 PM
makarius committed rISABELLE200ec7c4c1a5: tuned;.
tuned;
Sun, Mar 22, 3:12 PM

Sat, Mar 21

makarius created Blog Post: Slightly improved isabelle build_docker tool.
Sat, Mar 21, 10:42 PM
makarius committed rISABELLEf2c1154e9c8d: merged;.
merged;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLE9a364ed3a440: delete Isabelle distribution archive after use;.
delete Isabelle distribution archive after use;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEe9f53182c4aa: more NEWS;.
more NEWS;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLE9b49538845cc: documentation for "isabelle build_docker";.
documentation for "isabelle build_docker";
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEb0be6c0589e8: tuned bib;.
tuned bib;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEd59d557f4ee0: updated for release;.
updated for release;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEa9ec1a8bfd4a: more documentation on view.antiAlias, not just NEWS;.
more documentation on view.antiAlias, not just NEWS;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEaff37005fd79: more NEWS;.
more NEWS;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLE95460356d633: avoid premature crash due to missing session parents/imports;.
avoid premature crash due to missing session parents/imports;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEc67076c07fb8: avoid accidental update of base session sources (following documentation in….
avoid accidental update of base session sources (following documentation in…
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEf55222fbeae3: avoid duplicate stderr output in isabelle build -v, e.g. "Timing ..." (amending….
avoid duplicate stderr output in isabelle build -v, e.g. "Timing ..." (amending…
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEf36886cc32fa: prefer subpixel antialiasing by default: rendering of text is usually much….
prefer subpixel antialiasing by default: rendering of text is usually much…
Sat, Mar 21, 10:19 PM
makarius committed rISABELLEc2884545c846: slightly more explicit error, without going into the graph of proof futures;.
slightly more explicit error, without going into the graph of proof futures;
Sat, Mar 21, 10:19 PM
makarius committed rISABELLE391ea80ff27c: more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);.
more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);
Sat, Mar 21, 10:19 PM
makarius committed rISABELLE1005c50b2750: prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as….
prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as…
Sat, Mar 21, 10:18 PM
makarius committed rISABELLE9a29e883a934: tuned documentation, based on hints by Pedro Sánchez Terraf;.
tuned documentation, based on hints by Pedro Sánchez Terraf;
Sat, Mar 21, 10:18 PM
makarius committed rISABELLE76b739c0bedd: backed out changeset 7eadccd4392c: too confusing wrt. text overview panel;.
backed out changeset 7eadccd4392c: too confusing wrt. text overview panel;
Sat, Mar 21, 10:18 PM
makarius added a reverting change for rISABELLE7eadccd4392c: claried error elements: include internalized errors of tokens/commands;: rISABELLE76b739c0bedd: backed out changeset 7eadccd4392c: too confusing wrt. text overview panel;.
Sat, Mar 21, 10:18 PM

Fri, Mar 20

Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> committed rAFP1093d9d3d61f: Completed list of rules for differential invariance..
Completed list of rules for differential invariance.
Fri, Mar 20, 1:44 PM
paulson <lp15@cam.ac.uk> committed rAFPd556b9b6d06a: Some new and/or generalised theorems.
Some new and/or generalised theorems
Fri, Mar 20, 12:49 PM