equal
deleted
inserted
replaced
493 |
493 |
494 section {* Equivariance *} |
494 section {* Equivariance *} |
495 |
495 |
496 text {* |
496 text {* |
497 An important notion in the nominal logic work is |
497 An important notion in the nominal logic work is |
498 \emph{equivariance}. It will enable us to characterise how |
498 \emph{equivariance}. This notion allows us to characterise how |
499 permutations act upon compound statements in HOL by analysing how |
499 permutations act upon compound statements in HOL by analysing how |
500 these statements are constructed. To do so, let us first define |
500 these statements are constructed. To do so, let us first define |
501 \emph{HOL-terms}. They are given by the grammar |
501 \emph{HOL-terms}. They are given by the grammar |
502 |
502 |
503 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
503 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |