Fri, 13 Jan 2023 13:57:39 +0100 tuned;
wenzelm [Fri, 13 Jan 2023 13:57:39 +0100] rev 76962
tuned;
Fri, 13 Jan 2023 13:10:44 +0100 clarified default: final value is provided in Isabelle/Scala Latex.Cite.unapply;
wenzelm [Fri, 13 Jan 2023 13:10:44 +0100] rev 76961
clarified default: final value is provided in Isabelle/Scala Latex.Cite.unapply;
Fri, 13 Jan 2023 13:01:19 +0100 more "cite" antiquotations;
wenzelm [Fri, 13 Jan 2023 13:01:19 +0100] rev 76960
more "cite" antiquotations;
Fri, 13 Jan 2023 12:37:09 +0100 clarified signature: more generic operations;
wenzelm [Fri, 13 Jan 2023 12:37:09 +0100] rev 76959
clarified signature: more generic operations;
Fri, 13 Jan 2023 12:16:04 +0100 clarified check: this could be \nocite;
wenzelm [Fri, 13 Jan 2023 12:16:04 +0100] rev 76958
clarified check: this could be \nocite;
Thu, 12 Jan 2023 20:09:08 +0100 avoid confusion of markup element vs. property names;
wenzelm [Thu, 12 Jan 2023 20:09:08 +0100] rev 76957
avoid confusion of markup element vs. property names;
Thu, 12 Jan 2023 19:48:47 +0100 clarified Latex markup: optional cite "location" consists of nested document text;
wenzelm [Thu, 12 Jan 2023 19:48:47 +0100] rev 76956
clarified Latex markup: optional cite "location" consists of nested document text;
Thu, 12 Jan 2023 16:01:49 +0100 more explicit latex markup;
wenzelm [Thu, 12 Jan 2023 16:01:49 +0100] rev 76955
more explicit latex markup;
Wed, 11 Jan 2023 15:00:06 +0100 follow recent changes of Sledgehammer defaults, as 0a46b3dbd5ad exposes a hint in the source text;
wenzelm [Wed, 11 Jan 2023 15:00:06 +0100] rev 76954
follow recent changes of Sledgehammer defaults, as 0a46b3dbd5ad exposes a hint in the source text;
Sun, 15 Jan 2023 15:58:05 +0000 One messy, messy proof
paulson <lp15@cam.ac.uk> [Sun, 15 Jan 2023 15:58:05 +0000] rev 76953
One messy, messy proof
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 tip