Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. provide pre-built vscodium-1.65.2 for all platforms;
  3. tuned;
  4. provide vscode_extension via component, thus users don't need Node.js development tools; proper default for edit_extension; tuned messages;
  5. clarified options; tuned messages;
  6. Some new library lemmas
  7. merged
  8. really removing Dedekind_real
  9. merged
  10. Moving Dedekind_Real to the AFP
  11. tuned
  12. separated case reduction
  13. separated selector function entirely
  14. self-contained extraction auf clauses
  15. extracted selector function, restoring code generation for let expressions
  16. streamlined
  17. streamlined
  18. streamlined
  19. disentangled
Changeset 75336:4598cf29ef98 by wenzelm:
merged
Changeset 75335:381082508063 by wenzelm:
provide pre-built vscodium-1.65.2 for all platforms;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified NEWS (diff)
Changeset 75334:aeda3606c405 by wenzelm:
tuned;
The file was modified src/Tools/VSCode/src/vscode_main.scala (diff)
Changeset 75333:8f0d94fb8551 by wenzelm:
provide vscode_extension via component, thus users don&#039;t need Node.js development tools;<br>proper default for edit_extension;<br>tuned messages;
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
The file was modified src/Tools/VSCode/src/build_vscode_extension.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_main.scala (diff)
Changeset 75332:96a33aaf23a1 by wenzelm:
clarified options;<br>tuned messages;
The file was modified src/Tools/VSCode/src/build_vscode_extension.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_main.scala (diff)
Changeset 75331:c3f1bf2824bc by paulson _lp15@cam.ac.uk_:
Some new library lemmas
The file was modified src/HOL/Library/Equipollence.thy (diff)
Changeset 75330:bcb7d5f1f535 by paulson:
merged
Changeset 75329:1fb80d2a778d by paulson _lp15@cam.ac.uk_:
really removing Dedekind_real
The file was modified src/HOL/ROOT (diff)
Changeset 75328:fb8833d2c606 by paulson:
merged
Changeset 75327:f4a39342111b by paulson _lp15@cam.ac.uk_:
Moving Dedekind_Real to the AFP
The file was modified src/HOL/Real.thy (diff)
The file was removedsrc/HOL/ex/Dedekind_Real.thy
Changeset 75326:89d975dd39f1 by haftmann:
tuned
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75325:96da582011ae by haftmann:
separated case reduction
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75324:21897aad78ad by haftmann:
separated selector function entirely
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75323:a82f7f8a3c7b by haftmann:
self-contained extraction auf clauses
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75322:b7a74a04ae4e by haftmann:
extracted selector function, restoring code generation for let expressions
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75321:d06547c72775 by haftmann:
streamlined
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75320:fd3d66066256 by haftmann:
streamlined
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75319:c7ff16398535 by haftmann:
streamlined
The file was modified src/Tools/Code/code_thingol.ML (diff)
Changeset 75318:a2c5efb7298a by haftmann:
disentangled
The file was modified src/Tools/Code/code_thingol.ML (diff)