src/HOL/Mirabelle/Mirabelle_Test.thy
author wenzelm
Sat Sep 12 16:30:48 2009 +0200 (2009-09-12)
changeset 32564 378528d2f7eb
parent 32518 e3c4e337196c
child 38892 eccc9e2a6412
permissions -rw-r--r--
standard headers and text sections;
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
boehmes@32496
    10
  "Tools/mirabelle_arith.ML"
boehmes@32496
    11
  "Tools/mirabelle_metis.ML"
boehmes@32496
    12
  "Tools/mirabelle_quickcheck.ML"
boehmes@32496
    13
  "Tools/mirabelle_refute.ML"
boehmes@32496
    14
  "Tools/mirabelle_sledgehammer.ML"
boehmes@32496
    15
begin
boehmes@32496
    16
wenzelm@32564
    17
text {*
wenzelm@32564
    18
  Only perform type-checking of the actions,
wenzelm@32564
    19
  any reasonable test would be too complicated.
wenzelm@32564
    20
*}
boehmes@32496
    21
boehmes@32496
    22
end