--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 24 11:17:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Aug 24 11:17:33 2011 +0200
@@ -38,6 +38,7 @@
val trace : bool Config.T
val ignore_no_atp : bool Config.T
val instantiate_inducts : bool Config.T
+ val no_relevance_override : relevance_override
val const_names_in_fact :
theory -> (string * typ -> term list -> bool * term list) -> term
-> string list
@@ -100,6 +101,8 @@
del : (Facts.ref * Attrib.src list) list,
only : bool}
+val no_relevance_override = {add = [], del = [], only = false}
+
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
val abs_name = sledgehammer_prefix ^ "abs"
val skolem_prefix = sledgehammer_prefix ^ "sko"