| author | paulson <lp15@cam.ac.uk> |
| Wed, 17 Jul 2019 16:32:06 +0100 | |
| changeset 70367 | 81b65ddac59f |
| parent 62168 | e97452d79102 |
| permissions | -rw-r--r-- |
|
62168
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Eisbach/Eisbach_Old_Appl_Syntax.thy |
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
3 |
*) |
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
4 |
|
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
5 |
section \<open>Alternative Eisbach entry point for FOL, ZF etc.\<close> |
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
6 |
|
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
7 |
theory Eisbach_Old_Appl_Syntax |
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
8 |
imports Eisbach |
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
9 |
begin |
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
10 |
|
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
11 |
setup Pure_Thy.old_appl_syntax_setup |
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
12 |
|
|
e97452d79102
Eisbach works for other object-logics, e.g. Eisbach_FOL.thy;
wenzelm
parents:
diff
changeset
|
13 |
end |