src/HOL/Mirabelle/Mirabelle_Test.thy
author sultana
Sat Apr 14 23:52:17 2012 +0100 (2012-04-14)
changeset 47477 3fabf352243e
parent 41358 d5e91925916e
child 47730 15f4309bb9eb
permissions -rw-r--r--
renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
wenzelm@32564
     1
(*  Title:      HOL/Mirabelle/Mirabelle_Test.thy
wenzelm@32564
     2
    Author:     Sascha Boehme, TU Munich
boehmes@32496
     3
*)
boehmes@32496
     4
boehmes@32496
     5
header {* Simple test theory for Mirabelle actions *}
boehmes@32496
     6
boehmes@32518
     7
theory Mirabelle_Test
boehmes@32496
     8
imports Main Mirabelle
boehmes@32496
     9
uses
sultana@47477
    10
  "Actions/mirabelle_arith.ML"
sultana@47477
    11
  "Actions/mirabelle_metis.ML"
sultana@47477
    12
  "Actions/mirabelle_quickcheck.ML"
sultana@47477
    13
  "Actions/mirabelle_refute.ML"
sultana@47477
    14
  "Actions/mirabelle_sledgehammer.ML"
sultana@47477
    15
  "Actions/mirabelle_sledgehammer_filter.ML"
boehmes@32496
    16
begin
boehmes@32496
    17
wenzelm@32564
    18
text {*
wenzelm@32564
    19
  Only perform type-checking of the actions,
wenzelm@32564
    20
  any reasonable test would be too complicated.
wenzelm@32564
    21
*}
boehmes@32496
    22
boehmes@32496
    23
end