equal
deleted
inserted
replaced
809 \end{theorem} |
809 \end{theorem} |
810 |
810 |
811 \noindent |
811 \noindent |
812 This theorem states that the bound names do not appear in the support. |
812 This theorem states that the bound names do not appear in the support. |
813 For brevity we omit the proof and again refer the reader to |
813 For brevity we omit the proof and again refer the reader to |
814 our formalisation in Isabelle/HOL. |
814 our formalisation in Isabelle/HOL (or the appendix). |
815 |
815 |
816 %\noindent |
816 %\noindent |
817 %Below we will show the first equation. The others |
817 %Below we will show the first equation. The others |
818 %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
818 %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} |
819 %we have |
819 %we have |