wenzelm [Thu, 24 Mar 2022 22:27:17 +0100] rev 75333
provide vscode_extension via component, thus users don't need Node.js development tools;
proper default for edit_extension;
tuned messages;
wenzelm [Thu, 24 Mar 2022 20:45:14 +0100] rev 75332
clarified options;
tuned messages;
paulson <lp15@cam.ac.uk> [Thu, 24 Mar 2022 22:43:41 +0000] rev 75331
Some new library lemmas
paulson [Thu, 24 Mar 2022 22:21:24 +0000] rev 75330
merged
paulson <lp15@cam.ac.uk> [Thu, 24 Mar 2022 18:50:11 +0000] rev 75329
really removing Dedekind_real
paulson [Thu, 24 Mar 2022 18:28:51 +0000] rev 75328
merged
paulson <lp15@cam.ac.uk> [Thu, 24 Mar 2022 18:28:44 +0000] rev 75327
Moving Dedekind_Real to the AFP
haftmann [Thu, 24 Mar 2022 16:34:44 +0000] rev 75326
tuned
haftmann [Thu, 24 Mar 2022 16:34:43 +0000] rev 75325
separated case reduction
haftmann [Thu, 24 Mar 2022 16:34:42 +0000] rev 75324
separated selector function entirely
haftmann [Thu, 24 Mar 2022 16:34:41 +0000] rev 75323
self-contained extraction auf clauses
haftmann [Thu, 24 Mar 2022 16:34:40 +0000] rev 75322
extracted selector function, restoring code generation for let expressions
haftmann [Thu, 24 Mar 2022 16:34:39 +0000] rev 75321
streamlined
haftmann [Thu, 24 Mar 2022 16:34:38 +0000] rev 75320
streamlined