src/HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 62168 e97452d79102
permissions -rw-r--r--
more permissive;
     1 (*  Title:      HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy
     2     Author:     Makarius
     3 *)
     4 
     5 section \<open>Alternative Eisbach entry point for FOL, ZF etc.\<close>
     6 
     7 theory Eisbach_Old_Appl_Syntax
     8 imports Eisbach
     9 begin
    10 
    11 setup Pure_Thy.old_appl_syntax_setup
    12 
    13 end