src/HOL/Mirabelle/MirabelleTest.thy
author boehmes
Wed Sep 02 16:23:53 2009 +0200 (2009-09-02)
changeset 32496 4ab00a2642c3
permissions -rw-r--r--
moved Mirabelle from HOL/Tools to HOL,
added session HOL-Mirabelle
boehmes@32496
     1
(* Title: MirabelleTest.thy
boehmes@32496
     2
   Author: Sascha Boehme
boehmes@32496
     3
*)
boehmes@32496
     4
boehmes@32496
     5
header {* Simple test theory for Mirabelle actions *}
boehmes@32496
     6
boehmes@32496
     7
theory MirabelleTest
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
boehmes@32496
    17
(*
boehmes@32496
    18
  only perform type-checking of the actions,
boehmes@32496
    19
  any reasonable test would be too complicated
boehmes@32496
    20
*)
boehmes@32496
    21
boehmes@32496
    22
end