add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
(* Title: HOL/Hahn_Banach/ROOT.ML
Author: Gertrud Bauer, TU Munich
The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
*)
use_thys ["Hahn_Banach"];