- Queries
- All Stories
- Search
- Advanced Search
- Transactions
- Transaction Logs
Feed All Stories
All Stories
All Stories
Mar 31 2020
Mar 31 2020
Mar 30 2020
Mar 30 2020
Julian Brunner <julianbrunner@gmail.com> committed rAFPddaf86ffa226: merged.
merged
Julian Brunner <julianbrunner@gmail.com> committed rAFP744b282fd492: updated benchmarks.
updated benchmarks
Julian Brunner <julianbrunner@gmail.com> committed rAFP819a553f7508: using proper atomic propositions, added more benchmarks.
using proper atomic propositions, added more benchmarks
avoid nonterminal clash in syntax translation
clarified signature;
more accurate treatment of errors;
clarified modules: global quasi-scope for markers;
paulson <lp15@cam.ac.uk> committed rISABELLE2a24c2015a61: more ugly old proofs.
more ugly old proofs
Mar 29 2020
Mar 29 2020
clarified modules;
makarius committed rISABELLEb3bddebe44ca: clarified signature: more explicit type Protocol_Message.Marker;.
clarified signature: more explicit type Protocol_Message.Marker;
tuned signature -- follow Scala;
more explicit type Protocol_Message.Marker;
makarius committed rISABELLEe33f6e5f86b6: clarified protocol messages: explicitly use physical_writeln, always….
clarified protocol messages: explicitly use physical_writeln, always…
paulson <lp15@cam.ac.uk> committed rISABELLEa9de39608b1a: more tidying up of old apply-proofs.
more tidying up of old apply-proofs
Mar 28 2020
Mar 28 2020
eliminated pointless flag (see also 6533ceee4cd7);
paulson <lp15@cam.ac.uk> committed rISABELLE856c68ab6f13: structured a lot of ancient, horrible proofs.
structured a lot of ancient, horrible proofs
clarified Isabelle_Process phases;
clarified order: update syslog before handling exit;
tuned error message;
clarified signature: more robust startup_join;
Fixed some typos in Furstenberg_Topology
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd67fe5c0503b: website update.
website update
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP4c1cafe5bbdb: new entry: Furtenberg Topology.
new entry: Furtenberg Topology
nipkow committed rAFP7b6e642f98f1: New entry WOOT_Strong_Eventual_Consistency.
New entry WOOT_Strong_Eventual_Consistency
paulson <lp15@cam.ac.uk> committed rAFP50666eed97fe: Relational-Incorrectness-Logic website.
Relational-Incorrectness-Logic website
paulson <lp15@cam.ac.uk> committed rAFP270aae5bd0ac: new entry Relational-Incorrectness-Logic.
new entry Relational-Incorrectness-Logic
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb7b8b652815d: added new entry Hello_World.
added new entry Hello_World
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPf240cf67fc1f: sitegen + fix of ROOT file.
sitegen + fix of ROOT file
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPe87057e759a5: sitegen.
sitegen
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPad98c97b528c: new submission: VeriComp.
new submission: VeriComp
nipkow committed rAFP0b92dd22ffb1: New entry: Goodstein_Lambda.
New entry: Goodstein_Lambda
Mar 27 2020
Mar 27 2020
misc tuning based on hints by IntelliJ IDEA;
clarified signature;
clarified signature;
clarified signature;
clarified signature;
makarius committed rISABELLE01d92325ddab: clarified signature: more accurate session_base_info.sessions_structure;.
clarified signature: more accurate session_base_info.sessions_structure;
clarified signature;
Mar 25 2020
Mar 25 2020
paulson <lp15@cam.ac.uk> committed rISABELLE8e4d542f041b: updated to more modern style.
updated to more modern style
Mar 24 2020
Mar 24 2020
paulson <lp15@cam.ac.uk> committed rAFPdeab09fedc87: Grant acknowledgement for ALEXANDRIA (ERC Project 742178).
Grant acknowledgement for ALEXANDRIA (ERC Project 742178)
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.
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 on the mailing list some time after the Isabelle2020 release.
Asta Halkjær From <s144442@student.dtu.dk> committed rAFP8e310d6353b2: Update websites and emails..
Update websites and emails.
Asta Halkjær From <s144442@student.dtu.dk> committed rAFPc00714f311dc: Update abstract.
Update abstract
Mar 23 2020
Mar 23 2020
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…
updated to scala-2.12.11;
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
paulson <lp15@cam.ac.uk> committed rISABELLE4b1021677f15: tidying up some horrible proofs.
tidying up some horrible proofs
paulson <lp15@cam.ac.uk> committed rISABELLEe30dbfa53b0d: new-style Greater lemmas.
new-style Greater lemmas
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)
Mar 22 2020
Mar 22 2020
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…
paulson <lp15@cam.ac.uk> committed rAFP6bdf58e7175e: elimination of some aliases.
elimination of some aliases
paulson <lp15@cam.ac.uk> committed rAFP9bd18ac101a7: elimination of some aliases, etc..
elimination of some aliases, etc.
Mar 21 2020
Mar 21 2020
delete Isabelle distribution archive after use;
documentation for "isabelle build_docker";
updated for release;
more documentation on view.antiAlias, not just NEWS;
makarius committed rISABELLE95460356d633: avoid premature crash due to missing session parents/imports;.
avoid premature crash due to missing session parents/imports;
makarius committed rISABELLEc67076c07fb8: avoid accidental update of base session sources (following documentation in….
avoid accidental update of base session sources (following documentation in…
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…
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…
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;
makarius committed rISABELLE391ea80ff27c: more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);.
more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);
makarius committed rISABELLE1005c50b2750: prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as….
prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as…
makarius committed rISABELLE9a29e883a934: tuned documentation, based on hints by Pedro Sánchez Terraf;.
tuned documentation, based on hints by Pedro Sánchez Terraf;
makarius committed rISABELLE76b739c0bedd: backed out changeset 7eadccd4392c: too confusing wrt. text overview panel;.
backed out changeset 7eadccd4392c: too confusing wrt. text overview panel;
Mar 20 2020
Mar 20 2020
Jonathan Julian Huerta y Munive <jonjulian23@gmail.com> committed rAFP1093d9d3d61f: Completed list of rules for differential invariance..
Completed list of rules for differential invariance.
paulson <lp15@cam.ac.uk> committed rAFPd556b9b6d06a: Some new and/or generalised theorems.
Some new and/or generalised theorems