equal
deleted
inserted
replaced
39 (Output.writeln |
39 (Output.writeln |
40 (Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1 thm); |
40 (Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1 thm); |
41 (Seq.make_results (Seq.single (ctxt', thm)))))\<close> |
41 (Seq.make_results (Seq.single (ctxt', thm)))))\<close> |
42 |
42 |
43 ML \<open>fun method_evaluate text ctxt facts = |
43 ML \<open>fun method_evaluate text ctxt facts = |
44 Method.NO_CONTEXT_TACTIC ctxt |
44 NO_CONTEXT_TACTIC ctxt |
45 (Method.evaluate_runtime text ctxt facts)\<close> |
45 (Method.evaluate_runtime text ctxt facts)\<close> |
46 |
46 |
47 method_setup timeit = |
47 method_setup timeit = |
48 \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => |
48 \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => |
49 let |
49 let |