isabelle: src/HOL/TPTP/MaSh_Export_Base.thy@ca3ac5238c41 (annotated)

58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	1	(* Title: HOL/TPTP/MaSh_Export_Base.thy
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	3	*)
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	4
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	5	section \<open>MaSh Exporter Base\<close>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	6
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	7	theory MaSh_Export_Base
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	8	imports Main
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	9	begin
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	10
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 69597 diff changeset	11	ML_file \<open>mash_export.ML\<close>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	12
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	13	sledgehammer_params
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	14	[provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	15	lam_trans = lifting, timeout = 2, dont_preplay, minimize]
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	16
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	17	declare [[sledgehammer_fact_duplicates = true]]
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	18	declare [[sledgehammer_instantiate_inducts = false]]
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	19
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	20	hide_fact (open) HOL.ext
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	21
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	22	ML \<open>
62925 f1bdf10f95d8 tuned signature; wenzelm parents: 58889 diff changeset	23	Multithreading.max_threads ()
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	24	\<close>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	25
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	26	ML \<open>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	27	open MaSh_Export
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	28	\<close>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	29
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	30	ML \<open>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	31	val do_it = false (* switch to "true" to generate the files *)
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 63167 diff changeset	32	val thys = [\<^theory>\<open>List\<close>]
ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 63167 diff changeset	33	val params as {provers, ...} = Sledgehammer_Commands.default_params \<^theory> []
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	34	val prover = hd provers
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	35	val range = (1, NONE)
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	36	val step = 1
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	37	val max_suggestions = 1024
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	38	val dir = "List"
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	39	val prefix = "/tmp/" ^ dir ^ "/"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	40	\<close>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	41
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	42	end

author	haftmann
	Tue, 21 Apr 2020 07:28:17 +0000
changeset 71788	ca3ac5238c41
parent 69605	a96320074298
child 73942	57423714c29d
permissions	-rw-r--r--