# HG changeset patch
# User blanchet
# Date 1335392986 -7200
# Node ID 993a44ef99282dceaa974af5c63bdd19a170f717
# Parent  ba321ce6f344eaccae10b065ebdba22ba7fe87fe
tentatively tag hypotheses as definition -- this sometimes help the "tptp_sledgehammer" tool (e.g. SEU466^1.p)

diff -r ba321ce6f344 -r 993a44ef9928 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 26 00:28:06 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 26 00:29:46 2012 +0200
@@ -362,7 +362,7 @@
      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
    known_failures = known_szs_status_failures,
    conj_sym_kind = Axiom,
-   prem_kind = Hypothesis,
+   prem_kind = Definition (* motivated by "isabelle tptp_sledgehammer" tool *),
    best_slices =
      (* FUDGE *)
      K [(1.0, (true, ((100, satallax_thf0, "mono_native_higher", keep_lamsN, false), "")))]}