isabelle: src/HOL/TPTP/MaSh_Export_Base.thy@1c50ddcf6a01 (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
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	19	hide_fact (open) HOL.ext
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	20
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	21	ML \<open>
62925 f1bdf10f95d8 tuned signature; wenzelm parents: 58889 diff changeset	22	Multithreading.max_threads ()
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	23	\<close>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	24
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	25	ML \<open>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	26	open MaSh_Export
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	27	\<close>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	28
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	29	ML \<open>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	30	val do_it = false (* switch to "true" to generate the files *)
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 63167 diff changeset	31	val thys = [\<^theory>\<open>List\<close>]
ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 63167 diff changeset	32	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	33	val prover = hd provers
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	34	val range = (1, NONE)
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	35	val step = 1
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	36	val max_suggestions = 1024
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	37	val dir = "List"
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	38	val prefix = "/tmp/" ^ dir ^ "/"
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62925 diff changeset	39	\<close>
58206 3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	40
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	41	end

author	nipkow
	Thu, 09 Dec 2021 08:32:29 +0100
changeset 74888	1c50ddcf6a01
parent 73942	57423714c29d
permissions	-rw-r--r--