src/HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 62168 e97452d79102
permissions -rw-r--r--
more permissive;
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