src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML
changeset 32496 4ab00a2642c3
parent 32495 6decc1ffdbed
child 32497 922718ac81e4
     1.1 --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Wed Sep 02 16:02:37 2009 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,15 +0,0 @@
     1.4 -(* Title:  mirabelle_arith.ML
     1.5 -   Author: Jasmin Blanchette and Sascha Boehme
     1.6 -*)
     1.7 -
     1.8 -structure Mirabelle_Arith : MIRABELLE_ACTION =
     1.9 -struct
    1.10 -
    1.11 -fun arith_action {pre, timeout, log, ...} =
    1.12 -  if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
    1.13 -  then log "succeeded"
    1.14 -  else ()
    1.15 -
    1.16 -fun invoke _ = Mirabelle.register ("arith", arith_action)
    1.17 -
    1.18 -end