Changes

Summary

Tidied several ugly proofs in some elderly examples
tuned message;
clarified errors;
tuned messages;
support Node.js as well, reusing the engine from Electron/VSCodium;
updated to vscode 1.65.2;
proper result check;
merged
clarified directory layout and settings: more robust on all platforms;
tuned;
support Electron application framework; clarified vscodium startup;
generated lemma map_ident_strong for BNFs
updated SMT certificates
used more descriptive assert names in SMT-Lib output

Changeset 75287:7add2d5322a7 by paulson _lp15@cam.ac.uk_: Tidied several ugly proofs in some elderly examples
The file was modified	`src/HOL/Induct/QuoDataType.thy`
The file was modified	`src/HOL/Induct/QuoNestedDataType.thy`
Changeset 75286:29ee987174c0 by wenzelm: tuned message;
The file was modified	`lib/Tools/electron`
Changeset 75285:2b64d5657592 by wenzelm: clarified errors;
The file was modified	`lib/Tools/electron`
The file was modified	`lib/Tools/node`
The file was modified	`src/Tools/VSCode/src/vscode_setup.scala`
Changeset 75284:5417613efd74 by wenzelm: tuned messages;
The file was modified	`lib/Tools/electron`
The file was modified	`lib/Tools/node`
Changeset 75283:574fb6486c57 by wenzelm: support Node.js as well, reusing the engine from Electron/VSCodium;
The file was added	`lib/Tools/node`
Changeset 75282:249e900cc05f by wenzelm: updated to vscode 1.65.2;
The file was modified	`src/Tools/VSCode/etc/settings`
The file was modified	`src/Tools/VSCode/extension/package.json`
The file was modified	`src/Tools/VSCode/extension/yarn.lock`
Changeset 75281:fab9b0bd9715 by wenzelm: proper result check;
The file was modified	`src/Tools/VSCode/src/build_vscode_extension.scala`
Changeset 75280:b9dde91f9106 by wenzelm: merged
Changeset 75279:9229f2681db7 by wenzelm: clarified directory layout and settings: more robust on all platforms;
The file was modified	`lib/Tools/electron`
The file was modified	`lib/Tools/vscode`
The file was modified	`src/Tools/VSCode/extension/src/symbol.ts`
The file was modified	`src/Tools/VSCode/patches/cli.patch`
The file was modified	`src/Tools/VSCode/src/build_vscodium.scala`
Changeset 75278:249fde3aacbf by wenzelm: tuned;
The file was modified	`src/Tools/VSCode/src/build_vscodium.scala`
Changeset 75277:f64725832d63 by wenzelm: support Electron application framework;<br>clarified vscodium startup;
The file was added	`lib/Tools/electron`
The file was added	`src/Tools/VSCode/patches/cli.patch`
The file was modified	`lib/Tools/vscode`
The file was modified	`src/Tools/VSCode/extension/src/symbol.ts`
The file was modified	`src/Tools/VSCode/src/build_vscodium.scala`
Changeset 75276:686a6d7d0991 by desharna: generated lemma map_ident_strong for BNFs
The file was modified	`NEWS`
The file was modified	`src/Doc/Datatypes/Datatypes.thy`
The file was modified	`src/HOL/Tools/BNF/bnf_def.ML`
The file was modified	`src/HOL/Tools/BNF/bnf_def_tactics.ML`
Changeset 75275:cdb9c7d41a41 by desharna: updated SMT certificates
The file was modified	`src/HOL/SMT_Examples/Boogie_Dijkstra.certs`
The file was modified	`src/HOL/SMT_Examples/Boogie_Max.certs`
The file was modified	`src/HOL/SMT_Examples/SMT_Examples.certs`
The file was modified	`src/HOL/SMT_Examples/SMT_Examples_Verit.certs`
The file was modified	`src/HOL/SMT_Examples/SMT_Word_Examples.certs`
The file was modified	`src/HOL/SMT_Examples/VCC_Max.certs`
Changeset 75274:e89709b80b6e by desharna: used more descriptive assert names in SMT-Lib output
The file was modified	`src/HOL/Tools/SMT/cvc4_proof_parse.ML`
The file was modified	`src/HOL/Tools/SMT/smt_normalize.ML`
The file was modified	`src/HOL/Tools/SMT/smt_solver.ML`
The file was modified	`src/HOL/Tools/SMT/smt_translate.ML`
The file was modified	`src/HOL/Tools/SMT/smt_util.ML`
The file was modified	`src/HOL/Tools/SMT/smtlib_interface.ML`
The file was modified	`src/HOL/Tools/SMT/verit_isar.ML`
The file was modified	`src/HOL/Tools/SMT/verit_proof.ML`
The file was modified	`src/HOL/Tools/SMT/verit_proof_parse.ML`
The file was modified	`src/HOL/Tools/SMT/verit_replay.ML`
The file was modified	`src/HOL/Tools/lambda_lifting.ML`