changeset 73942 | 57423714c29d |
parent 69605 | a96320074298 |
--- a/src/HOL/TPTP/MaSh_Export_Base.thy Thu Jul 08 17:43:35 2021 +0200 +++ b/src/HOL/TPTP/MaSh_Export_Base.thy Fri Jul 09 17:58:17 2021 +0200 @@ -15,7 +15,6 @@ lam_trans = lifting, timeout = 2, dont_preplay, minimize] declare [[sledgehammer_fact_duplicates = true]] -declare [[sledgehammer_instantiate_inducts = false]] hide_fact (open) HOL.ext