src/HOL/Mirabelle/Mirabelle_Test.thy
author boehmes
Fri Sep 04 13:57:56 2009 +0200 (2009-09-04)
changeset 32518 e3c4e337196c
parent 32496 src/HOL/Mirabelle/MirabelleTest.thy@4ab00a2642c3
child 32564 378528d2f7eb
permissions -rw-r--r--
tuned
     1 (* Title: Mirabelle_Test.thy
     2    Author: Sascha Boehme
     3 *)
     4 
     5 header {* Simple test theory for Mirabelle actions *}
     6 
     7 theory Mirabelle_Test
     8 imports Main Mirabelle
     9 uses
    10   "Tools/mirabelle_arith.ML"
    11   "Tools/mirabelle_metis.ML"
    12   "Tools/mirabelle_quickcheck.ML"
    13   "Tools/mirabelle_refute.ML"
    14   "Tools/mirabelle_sledgehammer.ML"
    15 begin
    16 
    17 (*
    18   only perform type-checking of the actions,
    19   any reasonable test would be too complicated
    20 *)
    21 
    22 end