equal
deleted
inserted
replaced
7 theory Higher_Order_Logic |
7 theory Higher_Order_Logic |
8 imports Pure |
8 imports Pure |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 The following theory development illustrates the foundations of Higher-Order |
12 The following theory development illustrates the foundations of |
13 Logic. The ``HOL'' logic that is given here resembles \<^cite>\<open>"Gordon:1985:HOL"\<close> and its predecessor \<^cite>\<open>"church40"\<close>, but the order of |
13 Higher-Order Logic. The ``HOL'' logic that is given here resembles |
14 axiomatizations and defined connectives has be adapted to modern |
14 \<^cite>\<open>"Gordon:1985:HOL"\<close> and its predecessor \<^cite>\<open>"church40"\<close>, but |
15 presentations of \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits |
15 the order of axiomatizations and defined connectives has be adapted to |
16 nicely to the underlying Natural Deduction framework of Isabelle/Pure and |
16 modern presentations of \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus |
17 Isabelle/Isar. |
17 it fits nicely to the underlying Natural Deduction framework of |
|
18 Isabelle/Pure and Isabelle/Isar. |
18 \<close> |
19 \<close> |
19 |
20 |
20 |
21 |
21 section \<open>HOL syntax within Pure\<close> |
22 section \<open>HOL syntax within Pure\<close> |
22 |
23 |