isabelle: src/HOL/TPTP/MaSh_Eval.thy@7a78a74139f5 (annotated)

48285 902ab51dd12a renaming blanchet parents: 48284 diff changeset	1	(* Title: HOL/TPTP/MaSh_Eval.thy
48234 06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	3	*)
06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	4
48285 902ab51dd12a renaming blanchet parents: 48284 diff changeset	5	header {* MaSh Evaluation Driver *}
48234 06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	6
48285 902ab51dd12a renaming blanchet parents: 48284 diff changeset	7	theory MaSh_Eval
48333 2250197977dc repair MaSh exporter blanchet parents: 48322 diff changeset	8	imports Complex_Main
48234 06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	9	begin
06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	10
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48333 diff changeset	11	ML_file "mash_eval.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48333 diff changeset	12
48284 a3cb8901d60c clean up dependencies blanchet parents: 48251 diff changeset	13	sledgehammer_params
50402 923f1e199f4f use right names in MePo exporter blanchet parents: 50358 diff changeset	14	[provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
50358 b7d3319409b7 rationalized MaSh evaluation harness blanchet parents: 48891 diff changeset	15	lam_trans = combs_and_lifting, timeout = 15, dont_preplay, minimize]
48284 a3cb8901d60c clean up dependencies blanchet parents: 48251 diff changeset	16
48236 e174ecc4f5a4 instantiate induction rules blanchet parents: 48235 diff changeset	17	declare [[sledgehammer_instantiate_inducts]]
e174ecc4f5a4 instantiate induction rules blanchet parents: 48235 diff changeset	18
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	19	ML {*
48285 902ab51dd12a renaming blanchet parents: 48284 diff changeset	20	open MaSh_Eval
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	21	*}
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	22
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	23	ML {*
48333 2250197977dc repair MaSh exporter blanchet parents: 48322 diff changeset	24	val do_it = false (* switch to "true" to generate the files *)
48251 6cdcfbddc077 moved most of MaSh exporter code to Sledgehammer blanchet parents: 48250 diff changeset	25	val params = Sledgehammer_Isar.default_params @{context} []
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	26	*}
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	27
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	28	ML {*
48250 1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer) blanchet parents: 48245 diff changeset	29	if do_it then
50358 b7d3319409b7 rationalized MaSh evaluation harness blanchet parents: 48891 diff changeset	30	evaluate_mash_suggestions @{context} params "/tmp/mash_suggestions"
48250 1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer) blanchet parents: 48245 diff changeset	31	else
1065c307fafe further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer) blanchet parents: 48245 diff changeset	32	()
48235 40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	33	*}
40655464a93b MaSh evaluation driver blanchet parents: 48234 diff changeset	34
48234 06216c789ac9 moved MaSh into own files blanchet parents: diff changeset	35	end

author	wenzelm
	Fri, 07 Dec 2012 20:39:09 +0100
changeset 50428	7a78a74139f5
parent 50402	923f1e199f4f
child 50437	9762fe72936e
permissions	-rw-r--r--