equal
deleted
inserted
replaced
182 val ML_statistics: Properties.entry |
182 val ML_statistics: Properties.entry |
183 val task_statistics: Properties.entry |
183 val task_statistics: Properties.entry |
184 val command_timing: Properties.entry |
184 val command_timing: Properties.entry |
185 val loading_theory: string -> Properties.T |
185 val loading_theory: string -> Properties.T |
186 val dest_loading_theory: Properties.T -> string option |
186 val dest_loading_theory: Properties.T -> string option |
|
187 val use_theories_result: string -> bool -> Properties.T |
187 val simp_trace_logN: string |
188 val simp_trace_logN: string |
188 val simp_trace_stepN: string |
189 val simp_trace_stepN: string |
189 val simp_trace_recurseN: string |
190 val simp_trace_recurseN: string |
190 val simp_trace_hintN: string |
191 val simp_trace_hintN: string |
191 val simp_trace_ignoreN: string |
192 val simp_trace_ignoreN: string |
578 fun loading_theory name = [("function", "loading_theory"), ("name", name)]; |
579 fun loading_theory name = [("function", "loading_theory"), ("name", name)]; |
579 |
580 |
580 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name |
581 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name |
581 | dest_loading_theory _ = NONE; |
582 | dest_loading_theory _ = NONE; |
582 |
583 |
|
584 fun use_theories_result id ok = |
|
585 [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)]; |
|
586 |
583 |
587 |
584 (* simplifier trace *) |
588 (* simplifier trace *) |
585 |
589 |
586 val simp_trace_logN = "simp_trace_log"; |
590 val simp_trace_logN = "simp_trace_log"; |
587 val simp_trace_stepN = "simp_trace_step"; |
591 val simp_trace_stepN = "simp_trace_step"; |