| changeset 73691 | 2f9877db82a1 |
| parent 62519 | a564458f94db |
| child 73847 | 58f6b41efe88 |
| 73690:9267a04aabe6 | 73691:2f9877db82a1 |
|---|---|
1 (* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML |
|
2 Author: Jasmin Blanchette, TU Munich |
|
3 Author: Makarius |
|
4 |
|
5 Mirabelle action: "try0". |
|
6 *) |
|
7 |
|
8 structure Mirabelle_Try0 : sig end = |
|
9 struct |
|
10 |
|
11 val _ = |
|
12 Theory.setup (Mirabelle.command_action \<^binding>\<open>try0\<close> |
|
13 (fn {timeout, ...} => fn {pre, ...} => |
|
14 if Timeout.apply (Time.scale 10.0 timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre |
|
15 then "succeeded" else "")); |
|
16 |
|
17 end |