changeset 32496 | 4ab00a2642c3 |
parent 32472 | 7b92a8b8daaf |
child 32498 | 1132c7c13f36 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Wed Sep 02 16:23:53 2009 +0200 @@ -0,0 +1,15 @@ +(* Title: mirabelle_arith.ML + Author: Jasmin Blanchette and Sascha Boehme +*) + +structure Mirabelle_Arith : MIRABELLE_ACTION = +struct + +fun arith_action {pre, timeout, log, ...} = + if Mirabelle.can_apply timeout Arith_Data.arith_tac pre + then log "succeeded" + else () + +fun invoke _ = Mirabelle.register ("arith", arith_action) + +end