Changes

Summary

tuned;
tuned;
tuned comments;
more standard session build process, including browser_info; clarified final setup of global ML environment;
clarified files;
tuned;
proper support for recursive ML debugging;
tuned -- avoid recoding properties;

Changeset 62947:3374f3ffb2ec by wenzelm: tuned;
The file was modified	`src/Doc/Implementation/Integration.thy` (diff)
The file was modified	`src/HOL/Library/BigO.thy` (diff)
The file was modified	`src/HOL/Statespace/StateSpaceEx.thy` (diff)
Changeset 62946:9f537dd83677 by wenzelm: tuned;
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/Pure/Tools/build.scala` (diff)
Changeset 62945:c38c08889aa9 by wenzelm: tuned comments;
The file was modified	`src/Pure/General/socket_io.ML` (diff)
The file was modified	`src/Pure/ML/ml_profiling.ML` (diff)
The file was modified	`src/Pure/ML/ml_statistics.ML` (diff)
Changeset 62944:3ee643c5ed00 by wenzelm: more standard session build process, including browser_info;<br>clarified final setup of global ML environment;
The file was modified	`lib/html/library_index_content.template` (diff)
The file was modified	`src/Pure/ML/ml_compiler2.ML` (diff)
The file was modified	`src/Pure/ML_Bootstrap.thy` (diff)
The file was modified	`src/Pure/PIDE/session.ML` (diff)
The file was modified	`src/Pure/Pure.thy` (diff)
The file was modified	`src/Pure/ROOT` (diff)
The file was modified	`src/Pure/Thy/sessions.scala` (diff)
The file was modified	`src/Pure/Tools/build.scala` (diff)
The file was removed	`src/Pure/ML/ml_pervasive1.ML`
The file was removed	`src/Pure/ROOT1.ML`
Changeset 62943:659a8737501d by wenzelm: clarified files;
The file was added	`src/Pure/ML/ml_pervasive.ML`
The file was modified	`src/Pure/ROOT.ML` (diff)
The file was removed	`src/Pure/ML/ml_pervasive0.ML`
Changeset 62942:ba10c4e226cf by wenzelm: tuned;
The file was modified	`src/Pure/Thy/thy_info.ML` (diff)
Changeset 62941:5612ec9f0f49 by wenzelm: proper support for recursive ML debugging;
The file was modified	`src/Pure/ML/ml_compiler.ML` (diff)
The file was modified	`src/Pure/ML/ml_env.ML` (diff)
The file was modified	`src/Pure/ML/ml_recursive.ML` (diff)
Changeset 62940:a03592aafadf by wenzelm: tuned -- avoid recoding properties;
The file was modified	`src/Pure/Concurrent/thread_position.ML` (diff)
The file was modified	`src/Pure/General/position.ML` (diff)