author | wenzelm |
Thu, 22 Feb 2024 13:12:10 +0100 | |
changeset 79694 | ab7ec4a29b9c |
parent 78315 | addecc8de2c4 |
permissions | -rw-r--r-- |
78315 | 1 |
(* Title: Tools/profiling.ML |
2 |
Author: Makarius |
|
78314
1588bec693c2
copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff
changeset
|
3 |
|
78315 | 4 |
Session profiling based on loaded ML image. |
78314
1588bec693c2
copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff
changeset
|
5 |
*) |
1588bec693c2
copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff
changeset
|
6 |
|
78315 | 7 |
theory Profiling |
78314
1588bec693c2
copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff
changeset
|
8 |
imports Pure |
1588bec693c2
copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff
changeset
|
9 |
begin |
1588bec693c2
copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff
changeset
|
10 |
|
78315 | 11 |
ML_file "profiling.ML" |
12 |
ML_command \<open>Profiling.main ()\<close> |
|
78314
1588bec693c2
copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff
changeset
|
13 |
|
1588bec693c2
copy/rename files from private autocorres version e45b9b680d3e;
wenzelm
parents:
diff
changeset
|
14 |
end |