| changeset 66453 | cc19f7ca2ed6 |
| parent 62287 | 44bac8bebd9c |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 section \<open>Basic Eisbach examples (in FOL)\<close> |
5 section \<open>Basic Eisbach examples (in FOL)\<close> |
6 |
6 |
7 theory Examples_FOL |
7 theory Examples_FOL |
8 imports "~~/src/FOL/FOL" Eisbach_Old_Appl_Syntax |
8 imports FOL Eisbach_Old_Appl_Syntax |
9 begin |
9 begin |
10 |
10 |
11 |
11 |
12 subsection \<open>Basic methods\<close> |
12 subsection \<open>Basic methods\<close> |
13 |
13 |