wenzelm [Fri, 24 Feb 2023 11:07:31 +0100] rev 77363
unused (see also 7b318273a4aa and a1fb4d28e609);
paulson <lp15@cam.ac.uk> [Sat, 25 Feb 2023 17:35:48 +0000] rev 77362
tidying ugly proofs
nipkow [Fri, 24 Feb 2023 13:14:50 +0100] rev 77361
brought back [...] maplet syntax
paulson [Fri, 24 Feb 2023 10:59:59 +0000] rev 77360
merged
paulson <lp15@cam.ac.uk> [Thu, 23 Feb 2023 16:17:04 +0000] rev 77359
has_sum now an infix operator!!
paulson [Thu, 23 Feb 2023 15:21:22 +0000] rev 77358
merged
paulson <lp15@cam.ac.uk> [Thu, 23 Feb 2023 15:21:14 +0000] rev 77357
New material contributed by Manuel
nipkow [Thu, 23 Feb 2023 22:04:32 +0100] rev 77356
Map.empty no longer output abbreviation; %_. None is shorter and requires no explanation
desharna [Thu, 23 Feb 2023 15:37:17 +0100] rev 77355
added lemmas strict_subset_implies_multpDM and strict_subset_implies_multpHO
desharna [Thu, 23 Feb 2023 12:35:37 +0100] rev 77354
added lemma multpDM_plus_plusI[simp]
desharna [Thu, 23 Feb 2023 12:31:46 +0100] rev 77353
added lemmas multpDM_mono_strong and multpHO_mono_strong
paulson [Wed, 22 Feb 2023 22:01:26 +0000] rev 77352
merged
paulson <lp15@cam.ac.uk> [Wed, 22 Feb 2023 15:24:16 +0000] rev 77351
One new (necessary) theorem
wenzelm [Wed, 22 Feb 2023 21:40:32 +0100] rev 77350
merged
wenzelm [Wed, 22 Feb 2023 21:38:30 +0100] rev 77349
more operations to support management of jobs, e.g. from external database;