equal
deleted
inserted
replaced
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 *) |
3 *) |
4 |
4 |
5 section \<open>First-Order Formulas and the Definition of the Class L\<close> |
5 section \<open>First-Order Formulas and the Definition of the Class L\<close> |
6 |
6 |
7 theory Formula imports Main begin |
7 theory Formula imports ZF begin |
8 |
8 |
9 subsection\<open>Internalized formulas of FOL\<close> |
9 subsection\<open>Internalized formulas of FOL\<close> |
10 |
10 |
11 text\<open>De Bruijn representation. |
11 text\<open>De Bruijn representation. |
12 Unbound variables get their denotations from an environment.\<close> |
12 Unbound variables get their denotations from an environment.\<close> |