(* Title: HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy Author: Makarius *) section ‹Alternative Eisbach entry point for FOL, ZF etc.› theory Eisbach_Old_Appl_Syntax imports Eisbach begin setup Pure_Thy.old_appl_syntax_setup end