equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header {* The Full Theorem of Tarski *} |
8 header {* The Full Theorem of Tarski *} |
9 |
9 |
10 theory Tarski |
10 theory Tarski |
11 imports Main FuncSet |
11 imports Main "~~/src/HOL/Library/FuncSet" |
12 begin |
12 begin |
13 |
13 |
14 (*Many of these higher-order problems appear to be impossible using the |
14 (*Many of these higher-order problems appear to be impossible using the |
15 current linkup. They often seem to need either higher-order unification |
15 current linkup. They often seem to need either higher-order unification |
16 or explicit reasoning about connectives such as conjunction. The numerous |
16 or explicit reasoning about connectives such as conjunction. The numerous |