wenzelm [Thu, 04 Sep 2025 12:23:18 +0200] rev 83083
tuned comments;
wenzelm [Sat, 30 Aug 2025 13:45:06 +0200] rev 83082
partial update for vscodium-1.103.25610: only for linux;
wenzelm [Sat, 30 Aug 2025 13:10:55 +0200] rev 83081
more verbose;
wenzelm [Sat, 30 Aug 2025 13:07:29 +0200] rev 83080
more explicit messages, notably errors;
wenzelm [Sat, 30 Aug 2025 12:45:27 +0200] rev 83079
clarified signature: more explicit operations;
paulson <lp15@cam.ac.uk> [Sun, 07 Sep 2025 22:37:57 +0100] rev 83078
Removing "HOL-Library" as ancestor theory
paulson [Sun, 07 Sep 2025 17:42:10 +0100] rev 83077
merged
paulson <lp15@cam.ac.uk> [Sun, 07 Sep 2025 17:42:02 +0100] rev 83076
Some of Wenda Li's polynomial lemmas
haftmann [Sun, 07 Sep 2025 14:46:06 +0200] rev 83075
no need for "default" equations any longer
paulson <lp15@cam.ac.uk> [Sat, 06 Sep 2025 12:53:32 +0100] rev 83074
Removed needless [simp] attribute
paulson <lp15@cam.ac.uk> [Fri, 05 Sep 2025 21:53:19 +0100] rev 83073
Some lemmas moved in from Winding_Number_Eval
paulson <lp15@cam.ac.uk> [Wed, 03 Sep 2025 21:15:31 +0100] rev 83072
just cosmetic changes
haftmann [Wed, 03 Sep 2025 08:16:23 +0200] rev 83071
declare default code equations before custom attributes
haftmann [Sun, 31 Aug 2025 07:41:41 +0200] rev 83070
tuned
haftmann [Sat, 30 Aug 2025 18:01:46 +0200] rev 83069
prefer attribute for default singleton code equation
paulson [Sat, 30 Aug 2025 16:37:01 +0100] rev 83068
merged
paulson <lp15@cam.ac.uk> [Sat, 30 Aug 2025 16:36:51 +0100] rev 83067
Tidied a few messy proofs
paulson <lp15@cam.ac.uk> [Fri, 29 Aug 2025 16:51:55 +0100] rev 83066
tidied a few messy proofs
wenzelm [Thu, 28 Aug 2025 15:55:07 +0200] rev 83065
clarified show_results to serve as guard for interactive mode -- avoid printing internal consts, e.g. in 'record' or 'datatype', where Specification.definition is used as convenience for class instantiation (see also 889d5cdc034b, 951abf9db857, ecf80e37ed1a);
wenzelm [Thu, 28 Aug 2025 13:49:52 +0200] rev 83064
tuned whitespace;
wenzelm [Wed, 27 Aug 2025 20:42:15 +0200] rev 83063
JAWS works as well, e.g. using its free license for 40min;
tuned comments;
haftmann [Tue, 26 Aug 2025 20:26:12 +0200] rev 83062
explicit singleton default code equation declaration where appropriate
haftmann [Tue, 26 Aug 2025 18:59:06 +0200] rev 83061
preprocessing to execute bounded set comprehensions over tuples and triples
wenzelm [Mon, 25 Aug 2025 21:35:15 +0200] rev 83060
update jedit-20250825, according to patches;