isabelle: src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML@4dd63cf5bba5 (annotated)

49883 a6ebdaf8e267 added missing file blanchet parents: diff changeset	1	(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
a6ebdaf8e267 added missing file blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
a6ebdaf8e267 added missing file blanchet parents: diff changeset	3	Author: Steffen Juilf Smolka, TU Muenchen
a6ebdaf8e267 added missing file blanchet parents: diff changeset	4
49914 23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	5	Isar proof reconstruction from ATP proofs.
49883 a6ebdaf8e267 added missing file blanchet parents: diff changeset	6	*)
a6ebdaf8e267 added missing file blanchet parents: diff changeset	7
a6ebdaf8e267 added missing file blanchet parents: diff changeset	8	signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
a6ebdaf8e267 added missing file blanchet parents: diff changeset	9	sig
49914 23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	10	type 'a proof = 'a ATP_Proof.proof
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	11	type stature = ATP_Problem_Generate.stature
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	12
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	13	datatype reconstructor =
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	14	Metis of string * string \|
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	15	SMT
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	16
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	17	datatype play =
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	18	Played of reconstructor * Time.time \|
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	19	Trust_Playable of reconstructor * Time.time option \|
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	20	Failed_to_Play of reconstructor
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	21
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	22	type minimize_command = string list -> string
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	23	type one_line_params =
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	24	play * string * (string * stature) list * minimize_command * int * int
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	25	type isar_params =
50557 31313171deb5 thread no timeout properly blanchet parents: 50450 diff changeset	26	bool * bool * Time.time option * real * string Symtab.table
50004 c96e8e40d789 several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.) blanchet parents: 49994 diff changeset	27	* (string * stature) list vector * int Symtab.table * string proof * thm
49914 23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	28
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	29	val smtN : string
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	30	val string_for_reconstructor : reconstructor -> string
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	31	val lam_trans_from_atp_proof : string proof -> string -> string
23e36a4d28f1 refactor code blanchet parents: 49913 diff changeset	32	val is_typed_helper_used_in_atp_proof : string proof -> bool
23e36a4d28f1 refactor code blanchet parents: 49913

author	blanchet
	Wed, 20 Feb 2013 10:54:13 +0100
changeset 51198	4dd63cf5bba5
parent 51194	53a496954928
child 51200	260cb10aac4b
permissions	-rw-r--r--