| author | paulson | 
| Sat, 24 Aug 2024 14:14:57 +0100 | |
| changeset 80757 | 32f0e953cc96 | 
| parent 78315 | addecc8de2c4 | 
| child 82978 | 85c982ddc82d | 
| 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 |