isabelle: src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML@237d5be57277 (annotated)

52590 02713cd2c2cd tuned smolkas parents: 52555 diff changeset	1	(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
52555 6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	3	Author: Steffen Juilf Smolka, TU Muenchen
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	4
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	5	Reconstructors.
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	6	*)
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	7
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	8	signature SLEDGEHAMMER_RECONSTRUCTOR =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	9	sig
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	10	type stature = ATP_Problem_Generate.stature
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	11
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	12	datatype reconstructor =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	13	Metis of string * string \|
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	14	SMT
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	15
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	16	datatype play =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	17	Played of reconstructor * Time.time \|
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	18	Trust_Playable of reconstructor * Time.time option \|
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	19	Failed_to_Play of reconstructor
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	20
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	21	type minimize_command = string list -> string
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	22
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	23	type one_line_params =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	24	play * string * (string * stature) list * minimize_command * int * int
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	25
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	26	val smtN : string
54495 237d5be57277 refactored blanchet parents: 52590 diff changeset	27	end;
52555 6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	28
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	29	structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	30	struct
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	31
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	32	open ATP_Problem_Generate
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	33
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	34	datatype reconstructor =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	35	Metis of string * string \|
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	36	SMT
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	37
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	38	datatype play =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	39	Played of reconstructor * Time.time \|
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	40	Trust_Playable of reconstructor * Time.time option \|
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	41	Failed_to_Play of reconstructor
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	42
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	43	type minimize_command = string list -> string
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	44
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	45	type one_line_params =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	46	play * string * (string * stature) list * minimize_command * int * int
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	47
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	48	val smtN = "smt"
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	49
54495 237d5be57277 refactored blanchet parents: 52590 diff changeset	50	end;

author	blanchet
	Tue, 19 Nov 2013 16:48:50 +0100
changeset 54495	237d5be57277
parent 52590	02713cd2c2cd
child 54772	f5fd4a34b0e8
permissions	-rw-r--r--