Page MenuHomeIsabelle/Phabricator
Feed All Stories

Yesterday

Dominique Unruh <unruh@ut.ee> committed rAFP1145c2ed8f6c: Many changes to entry `Complex_Bounded_Operators`:.
Many changes to entry `Complex_Bounded_Operators`:
Mon, Oct 3, 1:12 PM

Sun, Oct 2

makarius updated the post content for Blog Post: Release Candidates for Isabelle2022.
Sun, Oct 2, 8:19 PM · isabelle-release
makarius committed rISABELLE6ab4bb7cb8b2: back to post-release mode -- after fork point;.
back to post-release mode -- after fork point;
Sun, Oct 2, 7:53 PM
makarius committed rISABELLE02c1ffc23d95: Added tag Isabelle2022-RC3 for changeset d704efeb01db.
Added tag Isabelle2022-RC3 for changeset d704efeb01db
Sun, Oct 2, 7:53 PM
makarius committed rISABELLEaa6ce2e51e6c: proper base names;.
proper base names;
Sun, Oct 2, 5:27 PM
makarius committed rISABELLEd704efeb01db: proper cygwin component (see d042947e47a3).
proper cygwin component (see d042947e47a3)
Sun, Oct 2, 5:27 PM
makarius committed rISABELLE30d43e9b2077: suppress command echo in output;.
suppress command echo in output;
Sun, Oct 2, 5:27 PM
makarius committed rISABELLEd042947e47a3: include openssh for rsync (see also a1c7829ac2de);.
include openssh for rsync (see also a1c7829ac2de);
Sun, Oct 2, 5:27 PM
makarius committed rISABELLE2a052820523d: provide naproche-20221002;.
provide naproche-20221002;
Sun, Oct 2, 5:27 PM

Sat, Oct 1

makarius committed rISABELLE0a44395a25f0: merged.
merged
Sat, Oct 1, 10:26 PM
makarius committed rISABELLE03dd2f19f1d7: clarified signature: more operations;.
clarified signature: more operations;
Sat, Oct 1, 10:26 PM
makarius committed rISABELLE16c12979c132: tuned signature;.
tuned signature;
Sat, Oct 1, 10:26 PM
makarius committed rISABELLE035ffcd82fb2: tuned, following hints by IntelliJ IDEA;.
tuned, following hints by IntelliJ IDEA;
Sat, Oct 1, 10:26 PM
makarius committed rISABELLEf3b23f4eaaac: clarified signature, to support external tools like "isabelle narration";.
clarified signature, to support external tools like "isabelle narration";
Sat, Oct 1, 10:26 PM
florian.haftmann committed rISABELLEa7ccb744047b: syntactic type classes for signed division operators.
syntactic type classes for signed division operators
Sat, Oct 1, 5:53 PM
florian.haftmann committed rAFPa74db29363f5: tuned proofs.
tuned proofs
Sat, Oct 1, 3:08 PM
florian.haftmann committed rISABELLE8a48e18f081e: reduce prominence of facts.
reduce prominence of facts
Sat, Oct 1, 3:08 PM
kleing committed rAFP6100f6dbbfed: merge from afp-2021-1.
merge from afp-2021-1
Sat, Oct 1, 11:14 AM
kleing committed rAFP2482f4650245: new entry Undirected_Graph_Theory.
new entry Undirected_Graph_Theory
Sat, Oct 1, 11:14 AM
nipkow committed rAFPa791f4f48a75: New entry: Maximum_Segment_Sum.
New entry: Maximum_Segment_Sum
Sat, Oct 1, 11:14 AM
nipkow committed rAFP8dd014d07166: typo.
typo
Sat, Oct 1, 11:14 AM
nipkow committed rAFP21836ba5b3e6: typo.
typo
Sat, Oct 1, 11:14 AM
Fabian Huch <huch@in.tum.de> committed rAFP549a8c591678: regenerate site;.
regenerate site;
Sat, Oct 1, 11:14 AM
nipkow committed rAFP25d277910e1a: added missing file.
added missing file
Sat, Oct 1, 11:14 AM
Fabian Huch <huch@in.tum.de> committed rAFP811ba4df645d: added topic for data management systems;.
added topic for data management systems;
Sat, Oct 1, 11:14 AM
nipkow committed rAFPd4348f7b41ae: New entry Safe_Range_RC.
New entry Safe_Range_RC
Sat, Oct 1, 11:14 AM

Fri, Sep 30

makarius committed rISABELLEfc19de122712: clarified signature;.
clarified signature;
Fri, Sep 30, 9:38 PM
makarius committed rISABELLE6ee5306d143a: more explanations on the new order prover (based on 10945fc183cd), without….
more explanations on the new order prover (based on 10945fc183cd), without…
Fri, Sep 30, 7:46 PM
makarius committed rISABELLE3c46356d241f: restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;.
restore NEWS, before commit accidents 2aad8698f82f and 10945fc183cd;
Fri, Sep 30, 7:46 PM
lukasstevens committed rISABELLE10945fc183cd: added documentation about new order prover.
added documentation about new order prover
Fri, Sep 30, 12:44 PM
lukasstevens committed rISABELLE2aad8698f82f: tweaked.
tweaked
Fri, Sep 30, 12:44 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEfb2be77a7819: tweaked;.
tweaked;
Fri, Sep 30, 9:28 AM

Thu, Sep 29

Fabian Huch <huch@in.tum.de> committed rAFP56381425e759: adjust Stalnaker_Logic to changes in Epistemic_Logic;.
adjust Stalnaker_Logic to changes in Epistemic_Logic;
Thu, Sep 29, 6:03 PM
florian.haftmann committed rAFP474696083e43: adjusted to distribution.
adjusted to distribution
Thu, Sep 29, 4:17 PM
florian.haftmann committed rISABELLE64e8d4afcf10: moved relevant theorems from theory Divides to theory Euclidean_Division.
moved relevant theorems from theory Divides to theory Euclidean_Division
Thu, Sep 29, 4:16 PM
Fabian Huch <huch@in.tum.de> committed rAFP6fce8550ee97: remove duplicate code;.
remove duplicate code;
Thu, Sep 29, 3:53 PM
Fabian Huch <huch@in.tum.de> committed rISABELLEbe91db94e526: amend jenkins ci build;.
amend jenkins ci build;
Thu, Sep 29, 2:16 PM
Fabian Huch <huch@in.tum.de> committed rISABELLE3c4e373922ca: restructured ci profile into modular ci build system;.
restructured ci profile into modular ci build system;
Thu, Sep 29, 2:09 PM
Fabian Huch <huch@in.tum.de> committed rAFP4c631c22d1d2: restructure afp ci builds (see Isabelle/3c4e373922ca).
restructure afp ci builds (see Isabelle/3c4e373922ca)
Thu, Sep 29, 2:08 PM

Wed, Sep 28

paulson <lp15@cam.ac.uk> committed rISABELLE1f2e78b7df93: more structured proofs.
more structured proofs
Wed, Sep 28, 8:15 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP4763f470b77d: Cosmetic changes..
Cosmetic changes.
Wed, Sep 28, 6:17 PM
paulson <lp15@cam.ac.uk> committed rISABELLEcf8f85e2a807: fixed some theory presentation issues (?).
fixed some theory presentation issues (?)
Wed, Sep 28, 12:24 PM
makarius committed rISABELLEcf7db6353322: recover informal "&" from 0c18df79b1c8;.
recover informal "&" from 0c18df79b1c8;
Wed, Sep 28, 12:24 PM

Tue, Sep 27

paulson <lp15@cam.ac.uk> committed rISABELLE728f38b016c0: added a couple of structured proofs.
added a couple of structured proofs
Tue, Sep 27, 11:57 PM
paulson <lp15@cam.ac.uk> committed rISABELLE8655344f1cf6: More obsolete "unfold" calls.
More obsolete "unfold" calls
Tue, Sep 27, 7:04 PM
paulson <lp15@cam.ac.uk> committed rISABELLEa642599ffdea: More syntactic cleanup. LaTeX markup working.
More syntactic cleanup. LaTeX markup working
Tue, Sep 27, 7:04 PM
paulson <lp15@cam.ac.uk> committed rISABELLE9fc34f76b4e8: getting rid of apply (unfold ...).
getting rid of apply (unfold ...)
Tue, Sep 27, 7:04 PM
paulson <lp15@cam.ac.uk> committed rISABELLE0c18df79b1c8: more modernisation of syntax.
more modernisation of syntax
Tue, Sep 27, 7:04 PM
paulson <lp15@cam.ac.uk> committed rISABELLEe44d86131648: Removal of obsolete ASCII syntax.
Removal of obsolete ASCII syntax
Tue, Sep 27, 7:04 PM
Fabian Huch <huch@in.tum.de> committed rAFPd81cfd823ae9: merge from afp-2021-1.
merge from afp-2021-1
Tue, Sep 27, 3:16 PM
Fabian Huch <huch@in.tum.de> committed rAFPd34f0b952a04: regenerate site;.
regenerate site;
Tue, Sep 27, 3:16 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP43747de4292f: web entry for Stalnaker_Logic.
web entry for Stalnaker_Logic
Tue, Sep 27, 3:16 PM
Fabian Huch <huch@in.tum.de> committed rAFPc1bc44c10400: afp site: minor stylistic improvements;.
afp site: minor stylistic improvements;
Tue, Sep 27, 3:16 PM
Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPe9bab02fb67c: new entry: Stalnaker Logic.
new entry: Stalnaker Logic
Tue, Sep 27, 3:16 PM
makarius committed rAFPa969a9029a5c: clarified options, following f2094906e491;.
clarified options, following f2094906e491;
Tue, Sep 27, 1:37 PM
makarius committed rISABELLEf2094906e491: clarified options;.
clarified options;
Tue, Sep 27, 1:36 PM

Mon, Sep 26

sterraf committed rAFP80e872e0fe3a: Comments on theories brought from ZF-Constructible. Shortening fm names.
Comments on theories brought from ZF-Constructible. Shortening fm names
Mon, Sep 26, 9:35 PM
makarius committed rISABELLE2802f6a4dd8b: merged.
merged
Mon, Sep 26, 8:49 PM
makarius committed rISABELLEe44e044dadb3: provide missing LaTeX macro, e.g. for AFP/PAC_Checker;.
provide missing LaTeX macro, e.g. for AFP/PAC_Checker;
Mon, Sep 26, 8:49 PM
makarius committed rISABELLE365f6a621fc5: clarified signature;.
clarified signature;
Mon, Sep 26, 8:49 PM
florian.haftmann committed rISABELLE14dd8b46307f: streamlined division on polynomials.
streamlined division on polynomials
Mon, Sep 26, 12:30 PM

Sun, Sep 25

florian.haftmann committed rISABELLE8fcbce9f317c: streamlined division on polynomials.
streamlined division on polynomials
Sun, Sep 25, 9:26 PM
florian.haftmann committed rAFP5e7974c944c6: adjusted to distribution.
adjusted to distribution
Sun, Sep 25, 9:16 PM

Sat, Sep 24

Asta Halkjær From <andro.from@gmail.com> committed rAFP2b82df697776: Remove fontenc from root.tex to make Ł show in PDF..
Remove fontenc from root.tex to make Ł show in PDF.
Sat, Sep 24, 11:00 AM

Fri, Sep 23

Asta Halkjær From <andro.from@gmail.com> committed rAFP189717e4b998: Update ROOT....
Update ROOT...
Fri, Sep 23, 8:26 PM
Asta Halkjær From <andro.from@gmail.com> committed rAFP611e8be50bec: Appendix with another axiom system as a variant of the proof..
Appendix with another axiom system as a variant of the proof.
Fri, Sep 23, 6:55 PM
kleing committed rAFPbd79c9c8cfa0: merge from afp-2021-1.
merge from afp-2021-1
Fri, Sep 23, 5:57 PM
kleing committed rAFP59f623140cfa: adapt to Isabelle@769a7cd5a16a.
adapt to Isabelle@769a7cd5a16a
Fri, Sep 23, 5:57 PM
kleing committed rAFP07172e9ae711: adjust Lar's contact info as requested.
adjust Lar's contact info as requested
Fri, Sep 23, 5:57 PM
pruvisto committed rAFP58d7766b8964: sitegen for Padic_Field.
sitegen for Padic_Field
Fri, Sep 23, 5:57 PM
pruvisto committed rAFPb4ba256202a1: sitegen for Risk_Free_Lending.
sitegen for Risk_Free_Lending
Fri, Sep 23, 5:57 PM
pruvisto committed rAFP802687e3f62a: new entry: Padic_Field.
new entry: Padic_Field
Fri, Sep 23, 5:57 PM
kleing committed rAFP7df5ba0f40af: new entry Implicational_Logic.
new entry Implicational_Logic
Fri, Sep 23, 5:57 PM
pruvisto committed rAFP7bce0418a16a: new entry: Risk_Free_Lending.
new entry: Risk_Free_Lending
Fri, Sep 23, 5:57 PM
nipkow committed rAFP1847e8b46ffd: New entry Separation_Logic_Unbounded.
New entry Separation_Logic_Unbounded
Fri, Sep 23, 5:57 PM
nipkow committed rAFPd076b363d88d: added web files.
added web files
Fri, Sep 23, 5:57 PM
nipkow committed rAFP0673c2f36b82: added web files.
added web files
Fri, Sep 23, 5:57 PM
nipkow committed rAFP8130283550b0: New entry SCC_Bloemen_Sequential.
New entry SCC_Bloemen_Sequential
Fri, Sep 23, 5:57 PM

Thu, Sep 22

makarius committed rISABELLE769a7cd5a16a: clarified signature: re-use store/cache from build results;.
clarified signature: re-use store/cache from build results;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLE005abcb34849: tuned signature;.
tuned signature;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLEd535db35388e: proper filter (amending fb4215da4919);.
proper filter (amending fb4215da4919);
Thu, Sep 22, 8:32 PM
makarius committed rISABELLEb80b2fbc46c3: clarified signature: persistent Node.source / Snapshot.source;.
clarified signature: persistent Node.source / Snapshot.source;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLE258056f533ce: more examples;.
more examples;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLE9d1819c28f67: clarified conditions: no_build is ok for presentation if "all_current" holds;.
clarified conditions: no_build is ok for presentation if "all_current" holds;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLE5266830ee9ec: tuned;.
tuned;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLE6bf42525f111: tuned signature;.
tuned signature;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLEfb4215da4919: clarified presentation_sessions: work with partial results;.
clarified presentation_sessions: work with partial results;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLE544e81a2c9fc: tuned signature: removed unused operations;.
tuned signature: removed unused operations;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLE19978abbc111: tuned;.
tuned;
Thu, Sep 22, 8:32 PM
makarius committed rISABELLEa1f458f089b9: tuned comments;.
tuned comments;
Thu, Sep 22, 8:32 PM

Wed, Sep 21

Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFPb9df51ee10b8: A few more disambiguations, related to locales in CartesianCategory..
A few more disambiguations, related to locales in CartesianCategory.
Wed, Sep 21, 6:59 PM
Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFP3abe8bbe58c0: Merged.
Merged
Wed, Sep 21, 3:27 PM
Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFP5996c6c489c3: Further disambiguation of facts to address clashes involving ConcreteCategory….
Further disambiguation of facts to address clashes involving ConcreteCategory…
Wed, Sep 21, 3:27 PM
florian.haftmann committed rISABELLEd435f7b57212: streamlined division on polynomials.
streamlined division on polynomials
Wed, Sep 21, 7:41 AM
florian.haftmann committed rAFPbccf6f281b7b: streamlined division on polynomials.
streamlined division on polynomials
Wed, Sep 21, 7:36 AM

Tue, Sep 20

Dominique Unruh <unruh@ut.ee> committed rAFP75a5ba7c00bc: Complex_Bounded_Operators: Fixed errors in document generation.
Complex_Bounded_Operators: Fixed errors in document generation
Tue, Sep 20, 1:54 PM
Dominique Unruh <unruh@ut.ee> committed rAFPc51cd33d81da: Complex_Bounded_Operators: Added numerous new lemmas..
Complex_Bounded_Operators: Added numerous new lemmas.
Tue, Sep 20, 1:01 PM

Mon, Sep 19

Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFP47f6b2669322: Disambiguate sufficiently many facts in locales so as to permit a top-level….
Disambiguate sufficiently many facts in locales so as to permit a top-level…
Mon, Sep 19, 9:05 PM
Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFP2d501ecd4932: Merged.
Merged
Mon, Sep 19, 9:05 PM
Eugene W. Stark <stark@cs.stonybrook.edu> committed rAFPf13ac4dee478: Fix a typo..
Fix a typo.
Mon, Sep 19, 9:05 PM