Sat, 14 Jan 2023 17:52:12 +0100 tuned;
wenzelm [Sat, 14 Jan 2023 17:52:12 +0100] rev 76968
tuned;
Fri, 13 Jan 2023 19:16:24 +0100 clarified types;
wenzelm [Fri, 13 Jan 2023 19:16:24 +0100] rev 76967
clarified types;
Fri, 13 Jan 2023 19:07:18 +0100 more explicit language context;
wenzelm [Fri, 13 Jan 2023 19:07:18 +0100] rev 76966
more explicit language context;
Fri, 13 Jan 2023 17:14:59 +0100 clarified signature: more explicit types;
wenzelm [Fri, 13 Jan 2023 17:14:59 +0100] rev 76965
clarified signature: more explicit types;
Fri, 13 Jan 2023 15:57:11 +0100 support embedded syntax, for use with control symbols;
wenzelm [Fri, 13 Jan 2023 15:57:11 +0100] rev 76964
support embedded syntax, for use with control symbols;
Fri, 13 Jan 2023 14:38:19 +0100 tuned;
wenzelm [Fri, 13 Jan 2023 14:38:19 +0100] rev 76963
tuned;
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
Sat, 14 Jan 2023 21:42:08 +0000 Missing theorem restored
paulson <lp15@cam.ac.uk> [Sat, 14 Jan 2023 21:42:08 +0000] rev 76952
Missing theorem restored
Sat, 14 Jan 2023 16:53:54 +0000 Tidying up BNF
paulson <lp15@cam.ac.uk> [Sat, 14 Jan 2023 16:53:54 +0000] rev 76951
Tidying up BNF
Fri, 13 Jan 2023 22:47:40 +0000 More cleaning up proofs, plus a TeX fix
paulson <lp15@cam.ac.uk> [Fri, 13 Jan 2023 22:47:40 +0000] rev 76950
More cleaning up proofs, plus a TeX fix
Fri, 13 Jan 2023 16:44:00 +0000 Fixed a broken proof
paulson <lp15@cam.ac.uk> [Fri, 13 Jan 2023 16:44:00 +0000] rev 76949
Fixed a broken proof
Fri, 13 Jan 2023 16:19:56 +0000 Substantial simplification of HOL-Cardinals
paulson <lp15@cam.ac.uk> [Fri, 13 Jan 2023 16:19:56 +0000] rev 76948
Substantial simplification of HOL-Cardinals
Fri, 13 Jan 2023 11:05:48 +0000 merged
paulson [Fri, 13 Jan 2023 11:05:48 +0000] rev 76947
merged
Thu, 12 Jan 2023 17:12:36 +0000 Trying to clean up HOL/Cardinals
paulson <lp15@cam.ac.uk> [Thu, 12 Jan 2023 17:12:36 +0000] rev 76946
Trying to clean up HOL/Cardinals
Thu, 12 Jan 2023 15:46:44 +0100 added session to mirabelle output directory structure
desharna [Thu, 12 Jan 2023 15:46:44 +0100] rev 76945
added session to mirabelle output directory structure
Wed, 11 Jan 2023 17:02:52 +0000 More tidying of topology proofs
paulson <lp15@cam.ac.uk> [Wed, 11 Jan 2023 17:02:52 +0000] rev 76944
More tidying of topology proofs
Wed, 11 Jan 2023 13:41:53 +0000 Partial round of clearing up applys, etc
paulson <lp15@cam.ac.uk> [Wed, 11 Jan 2023 13:41:53 +0000] rev 76943
Partial round of clearing up applys, etc
Tue, 10 Jan 2023 11:06:20 +0000 merged
paulson [Tue, 10 Jan 2023 11:06:20 +0000] rev 76942
merged
Mon, 09 Jan 2023 17:16:22 +0000 merged
paulson [Mon, 09 Jan 2023 17:16:22 +0000] rev 76941
merged
Mon, 09 Jan 2023 17:16:04 +0000 Substantial de-applying and streamlining
paulson <lp15@cam.ac.uk> [Mon, 09 Jan 2023 17:16:04 +0000] rev 76940
Substantial de-applying and streamlining
Mon, 09 Jan 2023 19:52:32 +0100 tuned sledgehammer default provers to only include local ones
desharna [Mon, 09 Jan 2023 19:52:32 +0100] rev 76939
tuned sledgehammer default provers to only include local ones
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 tip