isabelle: src/HOL/Tools/Mirabelle/mirabelle_try0.ML@2f9877db82a1 (annotated)

48740 d75450fe955a corrected header haftmann parents: 47942 diff changeset	1	(* Title: HOL/Mirabelle/Tools/mirabelle_try0.ML
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	2	Author: Jasmin Blanchette, TU Munich
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	3	Author: Makarius
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	4
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	5	Mirabelle action: "try0".
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	6	*)
e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	7
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	8	structure Mirabelle_Try0 : sig end =
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	9	struct
e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	10
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	11	val _ =
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	12	Theory.setup (Mirabelle.command_action \<^binding>\<open>try0\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	13	(fn {timeout, ...} => fn {pre, ...} =>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	14	if Timeout.apply (Time.scale 10.0 timeout) (Try0.try0 (SOME timeout) ([], [], [], [])) pre
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	15	then "succeeded" else ""));
47891 e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	16
e3627a83b114 added "try0" tool to Mirabelle blanchet parents: diff changeset	17	end

author	wenzelm
	Fri, 14 May 2021 21:32:11 +0200
changeset 73691	2f9877db82a1
parent 62519	src/HOL/Mirabelle/Tools/mirabelle_try0.ML@a564458f94db
child 73847	58f6b41efe88
permissions	-rw-r--r--