| author | boehmes |
| Wed, 02 Sep 2009 16:23:53 +0200 | |
| changeset 32496 | 4ab00a2642c3 |
| parent 32472 | src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML@7b92a8b8daaf |
| child 32498 | 1132c7c13f36 |
| permissions | -rw-r--r-- |
1 (* Title: mirabelle_arith.ML
2 Author: Jasmin Blanchette and Sascha Boehme
3 *)
5 structure Mirabelle_Arith : MIRABELLE_ACTION =
6 struct
8 fun arith_action {pre, timeout, log, ...} =
9 if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
10 then log "succeeded"
11 else ()
13 fun invoke _ = Mirabelle.register ("arith", arith_action)
15 end