wenzelm [Fri, 13 Jan 2023 14:38:19 +0100] rev 76963
tuned;
wenzelm [Fri, 13 Jan 2023 13:57:39 +0100] rev 76962
tuned;
wenzelm [Fri, 13 Jan 2023 13:10:44 +0100] rev 76961
clarified default: final value is provided in Isabelle/Scala Latex.Cite.unapply;
wenzelm [Fri, 13 Jan 2023 13:01:19 +0100] rev 76960
more "cite" antiquotations;
wenzelm [Fri, 13 Jan 2023 12:37:09 +0100] rev 76959
clarified signature: more generic operations;
wenzelm [Fri, 13 Jan 2023 12:16:04 +0100] rev 76958
clarified check: this could be \nocite;
wenzelm [Thu, 12 Jan 2023 20:09:08 +0100] rev 76957
avoid confusion of markup element vs. property names;
wenzelm [Thu, 12 Jan 2023 19:48:47 +0100] rev 76956
clarified Latex markup: optional cite "location" consists of nested document text;
wenzelm [Thu, 12 Jan 2023 16:01:49 +0100] rev 76955
more explicit latex markup;
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;
paulson <lp15@cam.ac.uk> [Sun, 15 Jan 2023 15:58:05 +0000] rev 76953
One messy, messy proof
paulson <lp15@cam.ac.uk> [Sat, 14 Jan 2023 21:42:08 +0000] rev 76952
Missing theorem restored
paulson <lp15@cam.ac.uk> [Sat, 14 Jan 2023 16:53:54 +0000] rev 76951
Tidying up BNF
paulson <lp15@cam.ac.uk> [Fri, 13 Jan 2023 22:47:40 +0000] rev 76950
More cleaning up proofs, plus a TeX fix
paulson <lp15@cam.ac.uk> [Fri, 13 Jan 2023 16:44:00 +0000] rev 76949
Fixed a broken proof