isabelle: src/HOL/Mirabelle.thy@2f9877db82a1 (annotated)

73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	1	(* Title: HOL/Mirabelle.thy
32564 378528d2f7eb standard headers and text sections; wenzelm parents: 32496 diff changeset	2	Author: Jasmin Blanchette and Sascha Boehme, TU Munich
32381 11542bebe4d4 made Mirabelle a component boehmes parents: diff changeset	3	*)
11542bebe4d4 made Mirabelle a component boehmes parents: diff changeset	4
11542bebe4d4 made Mirabelle a component boehmes parents: diff changeset	5	theory Mirabelle
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	6	imports Sledgehammer Predicate_Compile
32381 11542bebe4d4 made Mirabelle a component boehmes parents: diff changeset	7	begin
11542bebe4d4 made Mirabelle a component boehmes parents: diff changeset	8
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	9	ML_file \<open>Tools/Mirabelle/mirabelle.ML\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	10	ML_file \<open>Tools/Mirabelle/mirabelle_arith.ML\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	11	ML_file \<open>Tools/Mirabelle/mirabelle_metis.ML\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	12	ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	13	(*
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	14	ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer.ML\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	15	ML_file \<open>Tools/Mirabelle/mirabelle_sledgehammer_filter.ML\<close>
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	16	*)
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 73684 diff changeset	17	ML_file \<open>Tools/Mirabelle/mirabelle_try0.ML\<close>
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: 32383 diff changeset	18
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: 32383 diff changeset	19	end

author	wenzelm
	Fri, 14 May 2021 21:32:11 +0200
changeset 73691	2f9877db82a1
parent 73684	src/HOL/Mirabelle/Mirabelle.thy@a63d76ba0a03
child 73696	03e134d5f867
permissions	-rw-r--r--