src/HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy
author wenzelm
Wed Jan 13 16:41:32 2016 +0100 (2016-01-13)
changeset 62168 e97452d79102
permissions -rw-r--r--
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm@62168
     1
(*  Title:      HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy
wenzelm@62168
     2
    Author:     Makarius
wenzelm@62168
     3
*)
wenzelm@62168
     4
wenzelm@62168
     5
section \<open>Alternative Eisbach entry point for FOL, ZF etc.\<close>
wenzelm@62168
     6
wenzelm@62168
     7
theory Eisbach_Old_Appl_Syntax
wenzelm@62168
     8
imports Eisbach
wenzelm@62168
     9
begin
wenzelm@62168
    10
wenzelm@62168
    11
setup Pure_Thy.old_appl_syntax_setup
wenzelm@62168
    12
wenzelm@62168
    13
end