equal
deleted
inserted
replaced
5 structure Mirabelle_Arith : MIRABELLE_ACTION = |
5 structure Mirabelle_Arith : MIRABELLE_ACTION = |
6 struct |
6 struct |
7 |
7 |
8 fun arith_action {pre, timeout, log, ...} = |
8 fun arith_action {pre, timeout, log, ...} = |
9 if Mirabelle.can_apply timeout Arith_Data.arith_tac pre |
9 if Mirabelle.can_apply timeout Arith_Data.arith_tac pre |
10 then log "succeeded" |
10 then log "arith: succeeded" |
11 else () |
11 else () |
|
12 handle TimeLimit.TimeOut => log "arith: time out" |
12 |
13 |
13 fun invoke _ = Mirabelle.register ("arith", arith_action) |
14 fun invoke _ = Mirabelle.register ("arith", arith_action) |
14 |
15 |
15 end |
16 end |