isabelle: src/HOL/Mirabelle/Mirabelle_Test.thy@e62d5433bb47 (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
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	5	section \<open>Simple test theory for Mirabelle actions\<close>
32496 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	begin
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	10
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63167 diff changeset	11	ML_file \<open>Tools/mirabelle_arith.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63167 diff changeset	12	ML_file \<open>Tools/mirabelle_metis.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63167 diff changeset	13	ML_file \<open>Tools/mirabelle_quickcheck.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63167 diff changeset	14	ML_file \<open>Tools/mirabelle_refute.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63167 diff changeset	15	ML_file \<open>Tools/mirabelle_sledgehammer.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63167 diff changeset	16	ML_file \<open>Tools/mirabelle_sledgehammer_filter.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 63167 diff changeset	17	ML_file \<open>Tools/mirabelle_try0.ML\<close>
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47891 diff changeset	18
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	19	text \<open>
32564 378528d2f7eb standard headers and text sections; wenzelm parents: 32518 diff changeset	20	Only perform type-checking of the actions,
378528d2f7eb standard headers and text sections; wenzelm parents: 32518 diff changeset	21	any reasonable test would be too complicated.
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 58889 diff changeset	22	\<close>
32496 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	23
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: diff changeset	24	end

author	wenzelm
	Sat, 12 Oct 2019 16:46:33 +0200
changeset 70847	e62d5433bb47
parent 69605	a96320074298
child 73688	8c4ba5f61223
permissions	-rw-r--r--