isabelle: src/HOL/Mirabelle/Mirabelle_Test.thy@47d213b10fd7 (annotated)

32564 378528d2f7eb standard headers and text sections; wenzelm parents: 32518 diff changeset	1	(* Title: HOL/Mirabelle/Mirabelle_Test.thy
378528d2f7eb standard headers and text sections; wenzelm parents: 32518 diff changeset	2	Author: Sascha Boehme, TU Munich
32496 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	3	*)
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	4
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	5	header {* Simple test theory for Mirabelle actions *}
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	6
32518 e3c4e337196c tuned boehmes parents: 32496 diff changeset	7	theory Mirabelle_Test
32496 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	8	imports Main Mirabelle
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	9	uses
47730 15f4309bb9eb reversed Tools to Actions Mirabelle renaming; sultana parents: 47477 diff changeset	10	"Tools/mirabelle_arith.ML"
15f4309bb9eb reversed Tools to Actions Mirabelle renaming; sultana parents: 47477 diff changeset	11	"Tools/mirabelle_metis.ML"
15f4309bb9eb reversed Tools to Actions Mirabelle renaming; sultana parents: 47477 diff changeset	12	"Tools/mirabelle_quickcheck.ML"
15f4309bb9eb reversed Tools to Actions Mirabelle renaming; sultana parents: 47477 diff changeset	13	"Tools/mirabelle_refute.ML"
15f4309bb9eb reversed Tools to Actions Mirabelle renaming; sultana parents: 47477 diff changeset	14	"Tools/mirabelle_sledgehammer.ML"
15f4309bb9eb reversed Tools to Actions Mirabelle renaming; sultana parents: 47477 diff changeset	15	"Tools/mirabelle_sledgehammer_filter.ML"
32496 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	16	begin
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	17
32564 378528d2f7eb standard headers and text sections; wenzelm parents: 32518 diff changeset	18	text {*
378528d2f7eb standard headers and text sections; wenzelm parents: 32518 diff changeset	19	Only perform type-checking of the actions,
378528d2f7eb standard headers and text sections; wenzelm parents: 32518 diff changeset	20	any reasonable test would be too complicated.
378528d2f7eb standard headers and text sections; wenzelm parents: 32518 diff changeset	21	*}
32496 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	22
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	23	end

author	wenzelm
	Sun, 29 Apr 2012 23:08:27 +0200
changeset 47838	47d213b10fd7
parent 47730	15f4309bb9eb
child 47891	e3627a83b114
permissions	-rw-r--r--