Changes

Summary

prefer main entry points of HOL;
tuned signature;
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;

Changeset 67006:b1278ed3cd46 by wenzelm: prefer main entry points of HOL;
The file was modified	`src/HOL/Algebra/IntRing.thy` (diff)
The file was modified	`src/HOL/Analysis/L2_Norm.thy` (diff)
The file was modified	`src/HOL/Cardinals/Order_Union.thy` (diff)
The file was modified	`src/HOL/Cardinals/Wellfounded_More.thy` (diff)
The file was modified	`src/HOL/Library/Countable_Set_Type.thy` (diff)
The file was modified	`src/HOL/Library/FuncSet.thy` (diff)
The file was modified	`src/HOL/Library/ListVector.thy` (diff)
The file was modified	`src/HOL/Library/Option_ord.thy` (diff)
The file was modified	`src/HOL/Library/Preorder.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HSEQ.thy` (diff)
The file was modified	`src/HOL/Nonstandard_Analysis/HTranscendental.thy` (diff)
The file was modified	`src/HOL/ex/Birthday_Paradox.thy` (diff)
The file was modified	`src/HOL/ex/Groebner_Examples.thy` (diff)
The file was modified	`src/HOL/ex/PresburgerEx.thy` (diff)
Changeset 67005:11fca474d87a by wenzelm: tuned signature;
The file was modified	`src/Pure/Isar/outer_syntax.scala` (diff)
The file was modified	`src/Tools/VSCode/src/vscode_rendering.scala` (diff)
The file was modified	`src/Tools/jEdit/src/completion_popup.scala` (diff)
Changeset 67004:af72fa58f71b by wenzelm: clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
The file was modified	`src/Pure/General/completion.scala` (diff)
The file was modified	`src/Pure/Isar/outer_syntax.scala` (diff)
The file was modified	`src/Pure/System/options.scala` (diff)
The file was modified	`src/Pure/Thy/sessions.scala` (diff)
The file was modified	`src/Pure/Thy/thy_header.scala` (diff)
The file was modified	`src/Tools/VSCode/src/document_model.scala` (diff)
The file was modified	`src/Tools/jEdit/src/completion_popup.scala` (diff)
The file was modified	`src/Tools/jEdit/src/isabelle.scala` (diff)