isabelle: src/HOL/TPTP/MaSh_Export_Base.thy@205749fba102 (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
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	11	ML_file "mash_export.ML"
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 *)
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	32	val thys = [@{theory List}]
3e22d3ed829f refactored MaSh files to avoid regenerating exports on each eval blanchet parents: diff changeset	33	val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
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	paulson <lp15@cam.ac.uk>
	Sat, 21 Jul 2018 23:25:22 +0200
changeset 68671	205749fba102
parent 63167	0909deb8059b
child 69597	ff784d5a5bfb
permissions	-rw-r--r--