equal
deleted
inserted
replaced
3 |
3 |
4 Example that exercises Metis's and Sledgehammer's logical symbol proxies for |
4 Example that exercises Metis's and Sledgehammer's logical symbol proxies for |
5 rudimentary higher-order reasoning. |
5 rudimentary higher-order reasoning. |
6 *) |
6 *) |
7 |
7 |
8 header {* |
8 section {* |
9 Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for |
9 Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for |
10 Rudimentary Higher-Order Reasoning. |
10 Rudimentary Higher-Order Reasoning. |
11 *} |
11 *} |
12 |
12 |
13 theory Proxies |
13 theory Proxies |