wenzelm [Sat, 14 Jan 2023 17:52:12 +0100] rev 76968
tuned;
wenzelm [Fri, 13 Jan 2023 19:16:24 +0100] rev 76967
clarified types;
wenzelm [Fri, 13 Jan 2023 19:07:18 +0100] rev 76966
more explicit language context;
wenzelm [Fri, 13 Jan 2023 17:14:59 +0100] rev 76965
clarified signature: more explicit types;
wenzelm [Fri, 13 Jan 2023 15:57:11 +0100] rev 76964
support embedded syntax, for use with control symbols;
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
paulson <lp15@cam.ac.uk> [Fri, 13 Jan 2023 16:19:56 +0000] rev 76948
Substantial simplification of HOL-Cardinals
paulson [Fri, 13 Jan 2023 11:05:48 +0000] rev 76947
merged
paulson <lp15@cam.ac.uk> [Thu, 12 Jan 2023 17:12:36 +0000] rev 76946
Trying to clean up HOL/Cardinals
desharna [Thu, 12 Jan 2023 15:46:44 +0100] rev 76945
added session to mirabelle output directory structure
paulson <lp15@cam.ac.uk> [Wed, 11 Jan 2023 17:02:52 +0000] rev 76944
More tidying of topology proofs
paulson <lp15@cam.ac.uk> [Wed, 11 Jan 2023 13:41:53 +0000] rev 76943
Partial round of clearing up applys, etc
paulson [Tue, 10 Jan 2023 11:06:20 +0000] rev 76942
merged
paulson [Mon, 09 Jan 2023 17:16:22 +0000] rev 76941
merged
paulson <lp15@cam.ac.uk> [Mon, 09 Jan 2023 17:16:04 +0000] rev 76940
Substantial de-applying and streamlining
desharna [Mon, 09 Jan 2023 19:52:32 +0100] rev 76939
tuned sledgehammer default provers to only include local ones