src/HOL/Mirabelle/Mirabelle_Test.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 48891 c0eafbd55de3
child 58889 5b7a9633cfa8
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
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
begin
boehmes@32496
    10
wenzelm@48891
    11
ML_file "Tools/mirabelle_arith.ML"
wenzelm@48891
    12
ML_file "Tools/mirabelle_metis.ML"
wenzelm@48891
    13
ML_file "Tools/mirabelle_quickcheck.ML"
wenzelm@48891
    14
ML_file "Tools/mirabelle_refute.ML"
wenzelm@48891
    15
ML_file "Tools/mirabelle_sledgehammer.ML"
wenzelm@48891
    16
ML_file "Tools/mirabelle_sledgehammer_filter.ML"
wenzelm@48891
    17
ML_file "Tools/mirabelle_try0.ML"
wenzelm@48891
    18
wenzelm@32564
    19
text {*
wenzelm@32564
    20
  Only perform type-checking of the actions,
wenzelm@32564
    21
  any reasonable test would be too complicated.
wenzelm@32564
    22
*}
boehmes@32496
    23
boehmes@32496
    24
end